src/Pure/ML/ml_context.ML

--- a/src/Pure/ML/ml_context.ML	Mon Sep 06 21:33:19 2010 +0200
+++ b/src/Pure/ML/ml_context.ML	Mon Sep 06 22:08:49 2010 +0200
@@ -8,8 +8,6 @@
 sig
   val bind_thm: string * thm -> unit
   val bind_thms: string * thm list -> unit
-  val thm: xstring -> thm
-  val thms: xstring -> thm list
 end
 
 signature ML_CONTEXT =
@@ -18,6 +16,8 @@
   val the_generic_context: unit -> Context.generic
   val the_global_context: unit -> theory
   val the_local_context: unit -> Proof.context
+  val thm: xstring -> thm
+  val thms: xstring -> thm list
   val exec: (unit -> unit) -> Context.generic -> Context.generic
   val get_stored_thms: unit -> thm list
   val get_stored_thm: unit -> thm
@@ -49,6 +49,9 @@
 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 exec (e: unit -> unit) context =
   (case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of
     SOME context' => context'
@@ -89,9 +92,6 @@
 fun bind_thm (name, thm) = ml_store_thm (name, Drule.export_without_context thm);
 fun bind_thms (name, thms) = ml_store_thms (name, map Drule.export_without_context thms);
 
-fun thm name = ProofContext.get_thm (the_local_context ()) name;
-fun thms name = ProofContext.get_thms (the_local_context ()) name;
-
 
 
 (** ML antiquotations **)