# HG changeset patch
# User wenzelm
# Date 1283803729 -7200
# Node ID e7e12555e7637d50d44a200928a3fcffe48ddea7
# Parent  4d701c0388c303b56d849830dfd3a2d9de07f747
ML_Context.thm and ML_Context.thms no longer pervasive;

diff -r 4d701c0388c3 -r e7e12555e763 NEWS
--- a/NEWS	Mon Sep 06 21:33:19 2010 +0200
+++ b/NEWS	Mon Sep 06 22:08:49 2010 +0200
@@ -232,6 +232,10 @@
 * Configuration option show_question_marks only affects regular pretty
 printing of types and terms, not raw Term.string_of_vname.
 
+* ML_Context.thm and ML_Context.thms are no longer pervasive.  Rare
+INCOMPATIBILITY, superseded by static antiquotations @{thm} and
+@{thms} for most purposes.
+
 * ML structure Unsynchronized never opened, not even in Isar
 interaction mode as before.  Old Unsynchronized.set etc. have been
 discontinued -- use plain := instead.  This should be *rare* anyway,
diff -r 4d701c0388c3 -r e7e12555e763 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 **)