Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/specification.ML
changeset 59970 e9f73d87d904
parent 59844 c648efffea73
child 60377 234b7da8542e 
--- a/src/Pure/Isar/specification.ML	Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Apr 08 19:39:08 2015 +0200
@@ -356,7 +356,7 @@
         val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
         val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
 
-        val thesis = Object_Logic.fixed_judgment (Proof_Context.theory_of ctxt) Auto_Bind.thesisN;
+        val thesis = Object_Logic.fixed_judgment ctxt Auto_Bind.thesisN;
 
         fun assume_case ((name, (vars, _)), asms) ctxt' =
           let
isabelle