src/Pure/ML/ml_context.ML
changeset 42360 da8817d01e7c
parent 41485 6c0de045d127
child 43560 d1650e3720fd
--- a/src/Pure/ML/ml_context.ML	Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/ML/ml_context.ML	Sat Apr 16 15:47:52 2011 +0200
@@ -48,8 +48,8 @@
 val the_global_context = Context.theory_of o the_generic_context;
 val the_local_context = Context.proof_of o the_generic_context;
 
-fun thm name = ProofContext.get_thm (the_local_context ()) name;
-fun thms name = ProofContext.get_thms (the_local_context ()) name;
+fun thm name = Proof_Context.get_thm (the_local_context ()) name;
+fun thms name = Proof_Context.get_thms (the_local_context ()) name;
 
 fun exec (e: unit -> unit) context =
   (case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of