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/goal.ML
changeset 42360 da8817d01e7c
parent 41819 2d84831dc1a0
child 42370 244911efd275 
--- a/src/Pure/goal.ML	Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/goal.ML	Sat Apr 16 15:47:52 2011 +0200
@@ -154,7 +154,7 @@
 
 fun future_result ctxt result prop =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     val _ = Context.reject_draft thy;
     val cert = Thm.cterm_of thy;
     val certT = Thm.ctyp_of thy;
@@ -203,7 +203,7 @@
 
 fun prove_common immediate ctxt xs asms props tac =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     val string_of_term = Syntax.string_of_term ctxt;
 
     val pos = Position.thread_data ();
@@ -252,7 +252,7 @@
 fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
 
 fun prove_global thy xs asms prop tac =
-  Drule.export_without_context (prove (ProofContext.init_global thy) xs asms prop tac);
+  Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
isabelle