src/Pure/tactic.ML
changeset 12782 a4183c50ae5f
parent 12725 7ede865e1fe5
child 12801 a94cef8982cc
     1.1 --- a/src/Pure/tactic.ML	Wed Jan 16 22:23:46 2002 +0100
     1.2 +++ b/src/Pure/tactic.ML	Wed Jan 16 22:24:37 2002 +0100
     1.3 @@ -526,9 +526,11 @@
     1.4    (if Logic.is_norm_hhf (#prop (Thm.rep_thm th)) then th else rewrite_rule [Drule.norm_hhf_eq] th)
     1.5    |> Drule.gen_all;
     1.6  
     1.7 -val norm_hhf_tac = SUBGOAL (fn (t, i) =>
     1.8 -  if Logic.is_norm_hhf t then all_tac
     1.9 -  else rewrite_goal_tac [Drule.norm_hhf_eq] i);
    1.10 +val norm_hhf_tac =
    1.11 +  rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
    1.12 +  THEN' SUBGOAL (fn (t, i) =>
    1.13 +    if Logic.is_norm_hhf (Pattern.beta_eta_contract t) then all_tac
    1.14 +    else rewrite_goal_tac [Drule.norm_hhf_eq] i);
    1.15  
    1.16  
    1.17  (*** for folding definitions, handling critical pairs ***)