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