# HG changeset patch
# User wenzelm
# Date 1011216277 -3600
# Node ID a4183c50ae5f8df983ef60cf43687fc532301f81
# Parent  f76180d14819734aa656b13f0b5ced1eaee47c2c
tune norm_hhf_tac;

diff -r f76180d14819 -r a4183c50ae5f src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Jan 16 22:23:46 2002 +0100
+++ b/src/Pure/tactic.ML	Wed Jan 16 22:24:37 2002 +0100
@@ -526,9 +526,11 @@
   (if Logic.is_norm_hhf (#prop (Thm.rep_thm th)) then th else rewrite_rule [Drule.norm_hhf_eq] th)
   |> Drule.gen_all;
 
-val norm_hhf_tac = SUBGOAL (fn (t, i) =>
-  if Logic.is_norm_hhf t then all_tac
-  else rewrite_goal_tac [Drule.norm_hhf_eq] i);
+val norm_hhf_tac =
+  rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
+  THEN' SUBGOAL (fn (t, i) =>
+    if Logic.is_norm_hhf (Pattern.beta_eta_contract t) then all_tac
+    else rewrite_goal_tac [Drule.norm_hhf_eq] i);
 
 
 (*** for folding definitions, handling critical pairs ***)