src/Pure/Isar/element.ML
changeset 20007 8f9e6255108e
parent 19931 fb32b43e7f80
child 20058 7d035e26e5f9
     1.1 --- a/src/Pure/Isar/element.ML	Tue Jul 04 19:49:57 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Tue Jul 04 19:49:58 2006 +0200
     1.3 @@ -295,14 +295,22 @@
     1.4  
     1.5  (* derived rules *)
     1.6  
     1.7 -fun instantiate_tfrees thy subst =
     1.8 +fun instantiate_tfrees thy subst th =
     1.9    let
    1.10      val certT = Thm.ctyp_of thy;
    1.11 -    fun inst vs (a, T) = AList.lookup (op =) vs a
    1.12 -      |> Option.map (fn v => (certT (TVar v), certT T));
    1.13 +    val idx = Thm.maxidx_of th + 1;
    1.14 +    fun cert_inst (a, (S, T)) = (certT (TVar ((a, idx), S)), certT T);
    1.15 +
    1.16 +    fun add_inst (a, S) insts =
    1.17 +      if AList.defined (op =) insts a then insts
    1.18 +      else (case AList.lookup (op =) subst a of NONE => insts | SOME T => (a, (S, T)) :: insts);
    1.19 +    val insts =
    1.20 +      Term.fold_types (Term.fold_atyps (fn TFree v => add_inst v | _ => I))
    1.21 +        (Thm.full_prop_of th) [];
    1.22    in
    1.23 -    Drule.tvars_intr_list (map fst subst) #->
    1.24 -    (fn vs => Thm.instantiate (map_filter (inst vs) subst, []))
    1.25 +    th
    1.26 +    |> Thm.generalize (map fst insts, []) idx
    1.27 +    |> Thm.instantiate (map cert_inst insts, [])
    1.28    end;
    1.29  
    1.30  fun instantiate_frees thy subst =