diff options
| author | cp526 | 2015-06-05 14:25:09 +0100 |
|---|---|---|
| committer | cp526 | 2015-06-05 14:25:09 +0100 |
| commit | 2e19cb0d94b82a68eaf01fe3d4199d44b250191f (patch) | |
| tree | e44633604ef8f99ebe4e0e6dd333ed22b1f52b28 /src/lem_interp | |
| parent | 26d70608f82e48de73497ed84fa89b321d7864f3 (diff) | |
small variable renaming for Isabelle
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp.lem | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index de4938f8..ab7e8385 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -1136,8 +1136,8 @@ and vec_concat_match_plev t_level pat r_vals dir l last_pat t = then (true,false,eenv,r_vals,[]) else (false,false,eenv,[],[]) end) - | P_as (P_aux pat (l',Just(t,_,_,_))) id -> - let (matched_p, used_unknown, bounds,matcheds,r_vals) = vec_concat_match_plev t_level pat r_vals dir l last_pat t in + | P_as (P_aux pat (l',Just(t',_,_,_))) id -> + let (matched_p, used_unknown, bounds,matcheds,r_vals) = vec_concat_match_plev t_level pat r_vals dir l last_pat t' in if matched_p then (matched_p, used_unknown, (add_to_env (id,V_vector (if is_inc(dir) then 0 else (List.length matcheds)) dir matcheds) bounds), |