src/Pure/drule.ML
changeset 12719 41e0d086f8b6
parent 12710 d9e0674653b3
child 12725 7ede865e1fe5
     1.1 --- a/src/Pure/drule.ML	Fri Jan 11 14:44:58 2002 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Jan 11 14:53:05 2002 +0100
     1.3 @@ -315,10 +315,12 @@
     1.4  val forall_elim_var = PureThy.forall_elim_var;
     1.5  val forall_elim_vars = PureThy.forall_elim_vars;
     1.6  
     1.7 -fun forall_elim_vars_safe th =
     1.8 -  forall_elim_vars_safe (forall_elim_var (#maxidx (Thm.rep_thm th) + 1) th)
     1.9 -    handle THM _ => th;
    1.10 -
    1.11 +fun forall_elim_vars_safe thm =
    1.12 +  let
    1.13 +    val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
    1.14 +    fun elim (th, (x, T)) = Thm.forall_elim (Thm.cterm_of sign (Var ((x, maxidx + 1), T))) th;
    1.15 +    val vs = Term.strip_all_vars prop;
    1.16 +  in foldl elim (thm, Term.variantlist (map #1 vs, []) ~~ map #2 vs) end;
    1.17  
    1.18  (*Specialization over a list of cterms*)
    1.19  fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th);