src/Pure/Isar/specification.ML
changeset 35625 9c818cab0dd0
parent 35624 c4e29a0bb8c1
child 35894 ab6dc4d86ea1
     1.1 --- a/src/Pure/Isar/specification.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -316,7 +316,7 @@
     1.4          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
     1.5          val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
     1.6  
     1.7 -        val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) Auto_Bind.thesisN;
     1.8 +        val thesis = Object_Logic.fixed_judgment (ProofContext.theory_of ctxt) Auto_Bind.thesisN;
     1.9  
    1.10          fun assume_case ((name, (vars, _)), asms) ctxt' =
    1.11            let