src/Pure/tactic.ML
changeset 12725 7ede865e1fe5
parent 12498 3b0091bf06e8
child 12782 a4183c50ae5f
     1.1 --- a/src/Pure/tactic.ML	Fri Jan 11 18:49:25 2002 +0100
     1.2 +++ b/src/Pure/tactic.ML	Sat Jan 12 16:37:58 2002 +0100
     1.3 @@ -524,7 +524,7 @@
     1.4  
     1.5  fun norm_hhf th =
     1.6    (if Logic.is_norm_hhf (#prop (Thm.rep_thm th)) then th else rewrite_rule [Drule.norm_hhf_eq] th)
     1.7 -  |> Drule.forall_elim_vars_safe;
     1.8 +  |> Drule.gen_all;
     1.9  
    1.10  val norm_hhf_tac = SUBGOAL (fn (t, i) =>
    1.11    if Logic.is_norm_hhf t then all_tac