src/Pure/Isar/object_logic.ML
changeset 12725 7ede865e1fe5
parent 12479 ed46612ad7ec
child 12729 46808b5ec985
     1.1 --- a/src/Pure/Isar/object_logic.ML	Fri Jan 11 18:49:25 2002 +0100
     1.2 +++ b/src/Pure/Isar/object_logic.ML	Sat Jan 12 16:37:58 2002 +0100
     1.3 @@ -139,7 +139,7 @@
     1.4  
     1.5  fun gen_rulify full thm =
     1.6    Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm
     1.7 -  |> Drule.forall_elim_vars_safe |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
     1.8 +  |> Drule.gen_all |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
     1.9  
    1.10  val rulify = gen_rulify true;
    1.11  val rulify_no_asm = gen_rulify false;