src/Provers/blast.ML
changeset 35625 9c818cab0dd0
parent 35613 9d3ff36ad4e1
child 36001 992839c4be90
--- a/src/Provers/blast.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Provers/blast.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -181,7 +181,7 @@
 fun isGoal (Const ("*Goal*", _) $ _) = true
   | isGoal _ = false;
 
-val TruepropC = ObjectLogic.judgment_name Data.thy;
+val TruepropC = Object_Logic.judgment_name Data.thy;
 val TruepropT = Sign.the_const_type Data.thy TruepropC;
 
 fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);
@@ -1251,7 +1251,7 @@
 fun timing_depth_tac start cs lim i st0 =
   let val thy = Thm.theory_of_thm st0
       val state = initialize thy
-      val st = Conv.gconv_rule ObjectLogic.atomize_prems i st0
+      val st = Conv.gconv_rule Object_Logic.atomize_prems i st0
       val skoprem = fromSubgoal thy (List.nth(prems_of st, i-1))
       val hyps  = strip_imp_prems skoprem
       and concl = strip_imp_concl skoprem