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/proof.ML
changeset 59621 291934bac95e
parent 59616 eb59c6968219
child 59953 3d207f8f40dd 
--- a/src/Pure/Isar/proof.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Mar 06 15:58:56 2015 +0100
@@ -910,7 +910,7 @@
     val goal_propss = filter_out null propss';
     val goal =
       Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
-      |> Proof_Context.cterm_of ctxt
+      |> Thm.cterm_of ctxt
       |> Thm.weaken_sorts (Variable.sorts_of (context_of goal_state));
     val statement = ((kind, pos), propss', Thm.term_of goal);
     val after_qed' = after_qed |>> (fn after_local =>
isabelle