src/HOL/Tools/sat_funcs.ML
changeset 35625 9c818cab0dd0
parent 35408 b48ab741683b
child 38549 d0385f2764d8
     1.1 --- a/src/HOL/Tools/sat_funcs.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/sat_funcs.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -434,7 +434,7 @@
     1.4  
     1.5  val pre_cnf_tac =
     1.6          rtac ccontr THEN'
     1.7 -        ObjectLogic.atomize_prems_tac THEN'
     1.8 +        Object_Logic.atomize_prems_tac THEN'
     1.9          CONVERSION Drule.beta_eta_conversion;
    1.10  
    1.11  (* ------------------------------------------------------------------------- *)