# HG changeset patch
# User webertj
# Date 1146650753 -7200
# Node ID 9d15911f18938e2213ca9bdb63f03d6df9ff8e6b
# Parent  273d2c9866fdd2be8e16b9100a50b2db7f6849f5
pre_cnf_tac: beta-eta-normalization restricted to the current subgoal

diff -r 273d2c9866fd -r 9d15911f1893 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Wed May 03 09:45:09 2006 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Wed May 03 12:05:53 2006 +0200
@@ -336,13 +336,14 @@
 (*      (handling meta-logical connectives in B properly before negating),   *)
 (*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
 (*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
-(*      "-->", "!", and "="), then performs beta-eta-normalization           *)
+(*      "-->", "!", and "="), then performs beta-eta-normalization on the    *)
+(*      subgoal                                                              *)
 (* ------------------------------------------------------------------------- *)
 
 (* int -> Tactical.tactic *)
 
 fun pre_cnf_tac i = rtac ccontr i THEN ObjectLogic.atomize_tac i THEN
-  (fn st => Seq.single (Thm.equal_elim (Drule.beta_eta_conversion (cprop_of st)) st));
+                      PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (Drule.beta_eta_conversion)));
 
 (* ------------------------------------------------------------------------- *)
 (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)