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