# HG changeset patch # User wenzelm # Date 1152035398 -7200 # Node ID 8f9e6255108ec079c4c280ff98e63d326470ae3e # Parent 0f507e799938dbfbd82aff17f5c815a447cb901d instantiate_tfrees: Thm.generalize; diff -r 0f507e799938 -r 8f9e6255108e src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Tue Jul 04 19:49:57 2006 +0200 +++ b/src/Pure/Isar/element.ML Tue Jul 04 19:49:58 2006 +0200 @@ -295,14 +295,22 @@ (* derived rules *) -fun instantiate_tfrees thy subst = +fun instantiate_tfrees thy subst th = let val certT = Thm.ctyp_of thy; - fun inst vs (a, T) = AList.lookup (op =) vs a - |> Option.map (fn v => (certT (TVar v), certT T)); + val idx = Thm.maxidx_of th + 1; + fun cert_inst (a, (S, T)) = (certT (TVar ((a, idx), S)), certT T); + + fun add_inst (a, S) insts = + if AList.defined (op =) insts a then insts + else (case AList.lookup (op =) subst a of NONE => insts | SOME T => (a, (S, T)) :: insts); + val insts = + Term.fold_types (Term.fold_atyps (fn TFree v => add_inst v | _ => I)) + (Thm.full_prop_of th) []; in - Drule.tvars_intr_list (map fst subst) #-> - (fn vs => Thm.instantiate (map_filter (inst vs) subst, [])) + th + |> Thm.generalize (map fst insts, []) idx + |> Thm.instantiate (map cert_inst insts, []) end; fun instantiate_frees thy subst =