335 in |
335 in |
336 case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of |
336 case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of |
337 [] => (fth, fn x => x) |
337 [] => (fth, fn x => x) |
338 | vars => |
338 | vars => |
339 let fun newName (Var(ix,_), (pairs,used)) = |
339 let fun newName (Var(ix,_), (pairs,used)) = |
340 let val v = Name.variant used (string_of_indexname ix) |
340 let val v = singleton (Name.variant_list used) (string_of_indexname ix) |
341 in ((ix,v)::pairs, v::used) end; |
341 in ((ix,v)::pairs, v::used) end; |
342 val (alist, _) = List.foldr newName ([], Library.foldr OldTerm.add_term_names |
342 val (alist, _) = List.foldr newName ([], Library.foldr OldTerm.add_term_names |
343 (prop :: Thm.terms_of_tpairs tpairs, [])) vars |
343 (prop :: Thm.terms_of_tpairs tpairs, [])) vars |
344 fun mk_inst (Var(v,T)) = |
344 fun mk_inst (Var(v,T)) = |
345 (cterm_of thy (Var(v,T)), |
345 (cterm_of thy (Var(v,T)), |