1 (* Title: Tools/IsaPlanner/rw_inst.ML |
1 (* Title: Tools/IsaPlanner/rw_inst.ML |
2 ID: $Id$ |
|
3 Author: Lucas Dixon, University of Edinburgh |
2 Author: Lucas Dixon, University of Edinburgh |
4 |
3 |
5 Rewriting using a conditional meta-equality theorem which supports |
4 Rewriting using a conditional meta-equality theorem which supports |
6 schematic variable instantiation. |
5 schematic variable instantiation. |
7 *) |
6 *) |
141 val (conds_tyvs,cond_vs) = |
140 val (conds_tyvs,cond_vs) = |
142 Library.foldl (fn ((tyvs, vs), t) => |
141 Library.foldl (fn ((tyvs, vs), t) => |
143 (Library.union |
142 (Library.union |
144 (Term.term_tvars t, tyvs), |
143 (Term.term_tvars t, tyvs), |
145 Library.union |
144 Library.union |
146 (map Term.dest_Var (Term.term_vars t), vs))) |
145 (map Term.dest_Var (OldTerm.term_vars t), vs))) |
147 (([],[]), rule_conds); |
146 (([],[]), rule_conds); |
148 val termvars = map Term.dest_Var (Term.term_vars tgt); |
147 val termvars = map Term.dest_Var (OldTerm.term_vars tgt); |
149 val vars_to_fix = Library.union (termvars, cond_vs); |
148 val vars_to_fix = Library.union (termvars, cond_vs); |
150 val (renamings, names2) = |
149 val (renamings, names2) = |
151 foldr (fn (((n,i),ty), (vs, names')) => |
150 foldr (fn (((n,i),ty), (vs, names')) => |
152 let val n' = Name.variant names' n in |
151 let val n' = Name.variant names' n in |
153 ((((n,i),ty), Free (n', ty)) :: vs, n'::names') |
152 ((((n,i),ty), Free (n', ty)) :: vs, n'::names') |