# 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 **)