src/Provers/classical.ML

--- a/src/Provers/classical.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Provers/classical.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -153,7 +153,7 @@
 *)
 
 fun classical_rule rule =
-  if ObjectLogic.is_elim rule then
+  if Object_Logic.is_elim rule then
     let
       val rule' = rule RS classical;
       val concl' = Thm.concl_of rule';
@@ -173,7 +173,7 @@
   else rule;
 
 (*flatten nested meta connectives in prems*)
-val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 ObjectLogic.atomize_prems);
+val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 Object_Logic.atomize_prems);
 
 
 (*** Useful tactics for classical reasoning ***)
@@ -724,24 +724,24 @@
 
 (*Dumb but fast*)
 fun fast_tac cs =
-  ObjectLogic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
+  Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
 
 (*Slower but smarter than fast_tac*)
 fun best_tac cs =
-  ObjectLogic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
 
 (*even a bit smarter than best_tac*)
 fun first_best_tac cs =
-  ObjectLogic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
 
 fun slow_tac cs =
-  ObjectLogic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
 
 fun slow_best_tac cs =
-  ObjectLogic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
 
 
@@ -749,13 +749,13 @@
 val weight_ASTAR = Unsynchronized.ref 5;
 
 fun astar_tac cs =
-  ObjectLogic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL
     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
       (step_tac cs 1));
 
 fun slow_astar_tac cs =
-  ObjectLogic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL
     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
       (slow_step_tac cs 1));