99 bound vars with binders outside the redex *) |
99 bound vars with binders outside the redex *) |
100 val prop = Thm.prop_of rule; |
100 val prop = Thm.prop_of rule; |
101 val names = usednames_of_thm rule; |
101 val names = usednames_of_thm rule; |
102 val (fromnames,tonames,names2,Ts') = |
102 val (fromnames,tonames,names2,Ts') = |
103 Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => |
103 Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => |
104 let val n2 = Name.variant names n in |
104 let val n2 = singleton (Name.variant_list names) n in |
105 (ctermify (Free(faken,ty)) :: rnf, |
105 (ctermify (Free(faken,ty)) :: rnf, |
106 ctermify (Free(n2,ty)) :: rnt, |
106 ctermify (Free(n2,ty)) :: rnt, |
107 n2 :: names, |
107 n2 :: names, |
108 (n2,ty) :: Ts'') |
108 (n2,ty) :: Ts'') |
109 end) |
109 end) |
144 (([],[]), rule_conds); |
144 (([],[]), rule_conds); |
145 val termvars = map Term.dest_Var (OldTerm.term_vars tgt); |
145 val termvars = map Term.dest_Var (OldTerm.term_vars tgt); |
146 val vars_to_fix = union (op =) termvars cond_vs; |
146 val vars_to_fix = union (op =) termvars cond_vs; |
147 val (renamings, names2) = |
147 val (renamings, names2) = |
148 List.foldr (fn (((n,i),ty), (vs, names')) => |
148 List.foldr (fn (((n,i),ty), (vs, names')) => |
149 let val n' = Name.variant names' n in |
149 let val n' = singleton (Name.variant_list names') n in |
150 ((((n,i),ty), Free (n', ty)) :: vs, n'::names') |
150 ((((n,i),ty), Free (n', ty)) :: vs, n'::names') |
151 end) |
151 end) |
152 ([], names) vars_to_fix; |
152 ([], names) vars_to_fix; |
153 in renamings end; |
153 in renamings end; |
154 |
154 |
155 (* make a new fresh typefree instantiation for the given tvar *) |
155 (* make a new fresh typefree instantiation for the given tvar *) |
156 fun new_tfree (tv as (ix,sort), (pairs,used)) = |
156 fun new_tfree (tv as (ix,sort), (pairs,used)) = |
157 let val v = Name.variant used (string_of_indexname ix) |
157 let val v = singleton (Name.variant_list used) (string_of_indexname ix) |
158 in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end; |
158 in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end; |
159 |
159 |
160 |
160 |
161 (* make instantiations to fix type variables that are not |
161 (* make instantiations to fix type variables that are not |
162 already instantiated (in ignore_ixs) from the list of terms. *) |
162 already instantiated (in ignore_ixs) from the list of terms. *) |