365 [] => (fth, fn x => x) |
365 [] => (fth, fn x => x) |
366 | vars => |
366 | vars => |
367 let fun newName (Var(ix,_), (pairs,used)) = |
367 let fun newName (Var(ix,_), (pairs,used)) = |
368 let val v = Name.variant used (string_of_indexname ix) |
368 let val v = Name.variant used (string_of_indexname ix) |
369 in ((ix,v)::pairs, v::used) end; |
369 in ((ix,v)::pairs, v::used) end; |
370 val (alist, _) = List.foldr newName ([], Library.foldr add_term_names |
370 val (alist, _) = List.foldr newName ([], Library.foldr OldTerm.add_term_names |
371 (prop :: Thm.terms_of_tpairs tpairs, [])) vars |
371 (prop :: Thm.terms_of_tpairs tpairs, [])) vars |
372 fun mk_inst (Var(v,T)) = |
372 fun mk_inst (Var(v,T)) = |
373 (cterm_of thy (Var(v,T)), |
373 (cterm_of thy (Var(v,T)), |
374 cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T))) |
374 cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T))) |
375 val insts = map mk_inst vars |
375 val insts = map mk_inst vars |
803 |
803 |
804 (* var indexes *) |
804 (* var indexes *) |
805 |
805 |
806 (*Increment the indexes of only the type variables*) |
806 (*Increment the indexes of only the type variables*) |
807 fun incr_type_indexes inc th = |
807 fun incr_type_indexes inc th = |
808 let val tvs = term_tvars (prop_of th) |
808 let val tvs = OldTerm.term_tvars (prop_of th) |
809 and thy = theory_of_thm th |
809 and thy = Thm.theory_of_thm th |
810 fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s)) |
810 fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s)) |
811 in Thm.instantiate (map inc_tvar tvs, []) th end; |
811 in Thm.instantiate (map inc_tvar tvs, []) th end; |
812 |
812 |
813 fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1); |
813 fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1); |
814 |
814 |