changeset 23590 | ad95084a5c63 |
parent 23533 | b86b764d5764 |
child 26928 | ca87aff1ad2d |
--- a/src/HOL/Tools/sat_funcs.ML Thu Jul 05 19:59:01 2007 +0200 +++ b/src/HOL/Tools/sat_funcs.ML Thu Jul 05 20:01:26 2007 +0200 @@ -428,7 +428,7 @@ val pre_cnf_tac = rtac ccontr THEN' - ObjectLogic.atomize_tac THEN' + ObjectLogic.atomize_prems_tac THEN' CONVERSION Drule.beta_eta_conversion; (* ------------------------------------------------------------------------- *)