src/Pure/Isar/obtain.ML
changeset 35625 9c818cab0dd0
parent 33957 e9afca2118d4
child 35845 e5980f0ad025
     1.1 --- a/src/Pure/Isar/obtain.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -76,7 +76,7 @@
     1.4      val thy = ProofContext.theory_of fix_ctxt;
     1.5  
     1.6      val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
     1.7 -    val _ = ObjectLogic.is_judgment thy (Thm.concl_of thm) orelse
     1.8 +    val _ = Object_Logic.is_judgment thy (Thm.concl_of thm) orelse
     1.9        error "Conclusion in obtained context must be object-logic judgment";
    1.10  
    1.11      val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
    1.12 @@ -100,7 +100,7 @@
    1.13  fun bind_judgment ctxt name =
    1.14    let
    1.15      val (bind, ctxt') = ProofContext.bind_fixes [name] ctxt;
    1.16 -    val (t as _ $ Free v) = bind (ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name);
    1.17 +    val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (ProofContext.theory_of ctxt) name);
    1.18    in ((v, t), ctxt') end;
    1.19  
    1.20  val thatN = "that";