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