# HG changeset patch # User wenzelm # Date 1395137267 -3600 # Node ID 8e8d28ed752957d53efbc2e836b7063786b269e9 # Parent 21dd034523e533a18b7e362b12a38ccf894a3629 tuned signature -- rearranged modules; diff -r 21dd034523e5 -r 8e8d28ed7529 src/CCL/CCL.thy --- a/src/CCL/CCL.thy Tue Mar 18 10:00:23 2014 +0100 +++ b/src/CCL/CCL.thy Tue Mar 18 11:07:47 2014 +0100 @@ -295,9 +295,9 @@ val XH_to_Ds = map XH_to_D val XH_to_Es = map XH_to_E; -bind_thms ("ccl_rews", @{thms caseBs} @ @{thms ccl_injs} @ ccl_dstncts); -bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [@{thm notE}]); -bind_thms ("ccl_injDs", XH_to_Ds @{thms ccl_injs}); +ML_Thms.bind_thms ("ccl_rews", @{thms caseBs} @ @{thms ccl_injs} @ ccl_dstncts); +ML_Thms.bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [@{thm notE}]); +ML_Thms.bind_thms ("ccl_injDs", XH_to_Ds @{thms ccl_injs}); *} lemmas [simp] = ccl_rews diff -r 21dd034523e5 -r 8e8d28ed7529 src/CCL/Term.thy --- a/src/CCL/Term.thy Tue Mar 18 10:00:23 2014 +0100 +++ b/src/CCL/Term.thy Tue Mar 18 11:07:47 2014 +0100 @@ -286,7 +286,7 @@ subsection {* Constructors are distinct *} ML {* -bind_thms ("term_dstncts", +ML_Thms.bind_thms ("term_dstncts", mkall_dstnct_thms @{context} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs}) [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]); *} @@ -305,7 +305,7 @@ subsection {* Rewriting and Proving *} ML {* - bind_thms ("term_injDs", XH_to_Ds @{thms term_injs}); + ML_Thms.bind_thms ("term_injDs", XH_to_Ds @{thms term_injs}); *} lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews diff -r 21dd034523e5 -r 8e8d28ed7529 src/CCL/Type.thy --- a/src/CCL/Type.thy Tue Mar 18 10:00:23 2014 +0100 +++ b/src/CCL/Type.thy Tue Mar 18 11:07:47 2014 +0100 @@ -101,7 +101,7 @@ unfolding simp_type_defs by blast+ ML {* -bind_thms ("case_rls", XH_to_Es @{thms XHs}); +ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs}); *} @@ -262,7 +262,7 @@ lemmas iXHs = NatXH ListXH -ML {* bind_thms ("icase_rls", XH_to_Es @{thms iXHs}) *} +ML {* ML_Thms.bind_thms ("icase_rls", XH_to_Es @{thms iXHs}) *} subsection {* Type Rules *} @@ -340,7 +340,7 @@ (* - intro rules are type rules for canonical terms *) (* - elim rules are case rules (no non-canonical terms appear) *) -ML {* bind_thms ("XHEs", XH_to_Es @{thms XHs}) *} +ML {* ML_Thms.bind_thms ("XHEs", XH_to_Es @{thms XHs}) *} lemmas [intro!] = SubtypeI canTs icanTs and [elim!] = SubtypeE XHEs diff -r 21dd034523e5 -r 8e8d28ed7529 src/Doc/IsarImplementation/ML.thy --- a/src/Doc/IsarImplementation/ML.thy Tue Mar 18 10:00:23 2014 +0100 +++ b/src/Doc/IsarImplementation/ML.thy Tue Mar 18 11:07:47 2014 +0100 @@ -627,8 +627,8 @@ \begin{mldecls} @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\ @{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\ - @{index_ML bind_thms: "string * thm list -> unit"} \\ - @{index_ML bind_thm: "string * thm -> unit"} \\ + @{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\ + @{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\ \end{mldecls} \begin{description} @@ -642,12 +642,12 @@ \item @{ML "Context.>>"}~@{text f} applies context transformation @{text f} to the implicit context of the ML toplevel. - \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of + \item @{ML ML_Thms.bind_thms}~@{text "(name, thms)"} stores a list of theorems produced in ML both in the (global) theory context and the ML toplevel, associating it with the provided name. Theorems are put into a global ``standard'' format before being stored. - \item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a + \item @{ML ML_Thms.bind_thm} is similar to @{ML ML_Thms.bind_thms} but refers to a singleton fact. \end{description} diff -r 21dd034523e5 -r 8e8d28ed7529 src/FOLP/IFOLP.thy --- a/src/FOLP/IFOLP.thy Tue Mar 18 10:00:23 2014 +0100 +++ b/src/FOLP/IFOLP.thy Tue Mar 18 11:07:47 2014 +0100 @@ -411,7 +411,7 @@ done (*NOT PROVED -bind_thm ("ex1_cong", prove_goal (the_context ()) +ML_Thms.bind_thm ("ex1_cong", prove_goal (the_context ()) "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))" (fn prems => [ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1 diff -r 21dd034523e5 -r 8e8d28ed7529 src/HOL/Bali/AxSem.thy --- a/src/HOL/Bali/AxSem.thy Tue Mar 18 10:00:23 2014 +0100 +++ b/src/HOL/Bali/AxSem.thy Tue Mar 18 11:07:47 2014 +0100 @@ -1006,7 +1006,7 @@ apply (auto simp add: type_ok_def) done -ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt}) *} +ML {* ML_Thms.bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt}) *} declare ax_Abrupts [intro!] lemmas ax_Normal_cases = ax_cases [of _ _ _ normal] diff -r 21dd034523e5 -r 8e8d28ed7529 src/HOL/Bali/Eval.thy --- a/src/HOL/Bali/Eval.thy Tue Mar 18 10:00:23 2014 +0100 +++ b/src/HOL/Bali/Eval.thy Tue Mar 18 11:07:47 2014 +0100 @@ -745,7 +745,7 @@ *) ML {* -bind_thm ("eval_induct", rearrange_prems +ML_Thms.bind_thm ("eval_induct", rearrange_prems [0,1,2,8,4,30,31,27,15,16, 17,18,19,20,21,3,5,25,26,23,6, 7,11,9,13,14,12,22,10,28, @@ -881,7 +881,7 @@ | _ => SOME (mk_meta_eq @{thm eval_stmt_eq})) *} ML {* -bind_thms ("AbruptIs", sum3_instantiate @{context} @{thm eval.Abrupt}) +ML_Thms.bind_thms ("AbruptIs", sum3_instantiate @{context} @{thm eval.Abrupt}) *} declare halloc.Abrupt [intro!] eval.Abrupt [intro!] AbruptIs [intro!] diff -r 21dd034523e5 -r 8e8d28ed7529 src/HOL/Bali/Evaln.thy --- a/src/HOL/Bali/Evaln.thy Tue Mar 18 10:00:23 2014 +0100 +++ b/src/HOL/Bali/Evaln.thy Tue Mar 18 11:07:47 2014 +0100 @@ -292,7 +292,7 @@ (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *} -ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *} +ML {* ML_Thms.bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *} declare evaln_AbruptIs [intro!] lemma evaln_Callee: "G\Norm s\In1l (Callee l e)\\n\ (v,s') = False" diff -r 21dd034523e5 -r 8e8d28ed7529 src/HOL/Bali/Example.thy --- a/src/HOL/Bali/Example.thy Tue Mar 18 10:00:23 2014 +0100 +++ b/src/HOL/Bali/Example.thy Tue Mar 18 11:07:47 2014 +0100 @@ -894,7 +894,7 @@ declare member_is_static_simp [simp] declare wt.Skip [rule del] wt.Init [rule del] -ML {* bind_thms ("wt_intros", map (rewrite_rule @{context} @{thms id_def}) @{thms wt.intros}) *} +ML {* ML_Thms.bind_thms ("wt_intros", map (rewrite_rule @{context} @{thms id_def}) @{thms wt.intros}) *} lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros @@ -1187,7 +1187,7 @@ declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp] Base_foo_defs [simp] -ML {* bind_thms ("eval_intros", map +ML {* ML_Thms.bind_thms ("eval_intros", map (simplify (@{context} delsimps @{thms Skip_eq} addsimps @{thms lvar_def}) o rewrite_rule @{context} [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *} lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros diff -r 21dd034523e5 -r 8e8d28ed7529 src/HOL/Bali/Term.thy --- a/src/HOL/Bali/Term.thy Tue Mar 18 10:00:23 2014 +0100 +++ b/src/HOL/Bali/Term.thy Tue Mar 18 11:07:47 2014 +0100 @@ -262,7 +262,7 @@ is_stmt :: "term \ bool" where "is_stmt t = (\c. t=In1r c)" -ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *} +ML {* ML_Thms.bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *} declare is_stmt_rews [simp] diff -r 21dd034523e5 -r 8e8d28ed7529 src/HOL/UNITY/Comp/Alloc.thy --- a/src/HOL/UNITY/Comp/Alloc.thy Tue Mar 18 10:00:23 2014 +0100 +++ b/src/HOL/UNITY/Comp/Alloc.thy Tue Mar 18 11:07:47 2014 +0100 @@ -425,7 +425,7 @@ apply (rule fst_o_funPair) done -ML {* bind_thms ("fst_o_client_map'", make_o_equivs @{context} @{thm fst_o_client_map}) *} +ML {* ML_Thms.bind_thms ("fst_o_client_map'", make_o_equivs @{context} @{thm fst_o_client_map}) *} declare fst_o_client_map' [simp] lemma snd_o_client_map: "snd o client_map = clientState_d.dummy" @@ -433,7 +433,7 @@ apply (rule snd_o_funPair) done -ML {* bind_thms ("snd_o_client_map'", make_o_equivs @{context} @{thm snd_o_client_map}) *} +ML {* ML_Thms.bind_thms ("snd_o_client_map'", make_o_equivs @{context} @{thm snd_o_client_map}) *} declare snd_o_client_map' [simp] @@ -443,28 +443,28 @@ apply record_auto done -ML {* bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{context} @{thm client_o_sysOfAlloc}) *} +ML {* ML_Thms.bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{context} @{thm client_o_sysOfAlloc}) *} declare client_o_sysOfAlloc' [simp] lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv" apply record_auto done -ML {* bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfAlloc_eq}) *} +ML {* ML_Thms.bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfAlloc_eq}) *} declare allocGiv_o_sysOfAlloc_eq' [simp] lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk" apply record_auto done -ML {* bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfAlloc_eq}) *} +ML {* ML_Thms.bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfAlloc_eq}) *} declare allocAsk_o_sysOfAlloc_eq' [simp] lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel" apply record_auto done -ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfAlloc_eq}) *} +ML {* ML_Thms.bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfAlloc_eq}) *} declare allocRel_o_sysOfAlloc_eq' [simp] @@ -474,49 +474,49 @@ apply record_auto done -ML {* bind_thms ("client_o_sysOfClient'", make_o_equivs @{context} @{thm client_o_sysOfClient}) *} +ML {* ML_Thms.bind_thms ("client_o_sysOfClient'", make_o_equivs @{context} @{thm client_o_sysOfClient}) *} declare client_o_sysOfClient' [simp] lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd " apply record_auto done -ML {* bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfClient_eq}) *} +ML {* ML_Thms.bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfClient_eq}) *} declare allocGiv_o_sysOfClient_eq' [simp] lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd " apply record_auto done -ML {* bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfClient_eq}) *} +ML {* ML_Thms.bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfClient_eq}) *} declare allocAsk_o_sysOfClient_eq' [simp] lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd " apply record_auto done -ML {* bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfClient_eq}) *} +ML {* ML_Thms.bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfClient_eq}) *} declare allocRel_o_sysOfClient_eq' [simp] lemma allocGiv_o_inv_sysOfAlloc_eq: "allocGiv o inv sysOfAlloc = allocGiv" apply (simp add: o_def) done -ML {* bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_inv_sysOfAlloc_eq}) *} +ML {* ML_Thms.bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_inv_sysOfAlloc_eq}) *} declare allocGiv_o_inv_sysOfAlloc_eq' [simp] lemma allocAsk_o_inv_sysOfAlloc_eq: "allocAsk o inv sysOfAlloc = allocAsk" apply (simp add: o_def) done -ML {* bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_inv_sysOfAlloc_eq}) *} +ML {* ML_Thms.bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_inv_sysOfAlloc_eq}) *} declare allocAsk_o_inv_sysOfAlloc_eq' [simp] lemma allocRel_o_inv_sysOfAlloc_eq: "allocRel o inv sysOfAlloc = allocRel" apply (simp add: o_def) done -ML {* bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_inv_sysOfAlloc_eq}) *} +ML {* ML_Thms.bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_inv_sysOfAlloc_eq}) *} declare allocRel_o_inv_sysOfAlloc_eq' [simp] lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) = @@ -524,7 +524,7 @@ apply (simp add: o_def drop_map_def) done -ML {* bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{context} @{thm rel_inv_client_map_drop_map}) *} +ML {* ML_Thms.bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{context} @{thm rel_inv_client_map_drop_map}) *} declare rel_inv_client_map_drop_map [simp] lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) = @@ -532,7 +532,7 @@ apply (simp add: o_def drop_map_def) done -ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{context} @{thm ask_inv_client_map_drop_map}) *} +ML {* ML_Thms.bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{context} @{thm ask_inv_client_map_drop_map}) *} declare ask_inv_client_map_drop_map [simp] @@ -549,13 +549,13 @@ @{thm Client} |> simplify (@{context} addsimps @{thms client_spec_simps}) |> list_of_Int; -bind_thm ("Client_Increasing_ask", Client_Increasing_ask); -bind_thm ("Client_Increasing_rel", Client_Increasing_rel); -bind_thm ("Client_Bounded", Client_Bounded); -bind_thm ("Client_Progress", Client_Progress); -bind_thm ("Client_AllowedActs", Client_AllowedActs); -bind_thm ("Client_preserves_giv", Client_preserves_giv); -bind_thm ("Client_preserves_dummy", Client_preserves_dummy); +ML_Thms.bind_thm ("Client_Increasing_ask", Client_Increasing_ask); +ML_Thms.bind_thm ("Client_Increasing_rel", Client_Increasing_rel); +ML_Thms.bind_thm ("Client_Bounded", Client_Bounded); +ML_Thms.bind_thm ("Client_Progress", Client_Progress); +ML_Thms.bind_thm ("Client_AllowedActs", Client_AllowedActs); +ML_Thms.bind_thm ("Client_preserves_giv", Client_preserves_giv); +ML_Thms.bind_thm ("Client_preserves_dummy", Client_preserves_dummy); *} declare @@ -579,13 +579,13 @@ @{thm Network} |> simplify (@{context} addsimps @{thms network_spec_simps}) |> list_of_Int; -bind_thm ("Network_Ask", Network_Ask); -bind_thm ("Network_Giv", Network_Giv); -bind_thm ("Network_Rel", Network_Rel); -bind_thm ("Network_AllowedActs", Network_AllowedActs); -bind_thm ("Network_preserves_allocGiv", Network_preserves_allocGiv); -bind_thm ("Network_preserves_rel", Network_preserves_rel); -bind_thm ("Network_preserves_ask", Network_preserves_ask); +ML_Thms.bind_thm ("Network_Ask", Network_Ask); +ML_Thms.bind_thm ("Network_Giv", Network_Giv); +ML_Thms.bind_thm ("Network_Rel", Network_Rel); +ML_Thms.bind_thm ("Network_AllowedActs", Network_AllowedActs); +ML_Thms.bind_thm ("Network_preserves_allocGiv", Network_preserves_allocGiv); +ML_Thms.bind_thm ("Network_preserves_rel", Network_preserves_rel); +ML_Thms.bind_thm ("Network_preserves_ask", Network_preserves_ask); *} declare Network_preserves_allocGiv [iff] @@ -610,13 +610,13 @@ @{thm Alloc} |> simplify (@{context} addsimps @{thms alloc_spec_simps}) |> list_of_Int; -bind_thm ("Alloc_Increasing_0", Alloc_Increasing_0); -bind_thm ("Alloc_Safety", Alloc_Safety); -bind_thm ("Alloc_Progress", Alloc_Progress); -bind_thm ("Alloc_AllowedActs", Alloc_AllowedActs); -bind_thm ("Alloc_preserves_allocRel", Alloc_preserves_allocRel); -bind_thm ("Alloc_preserves_allocAsk", Alloc_preserves_allocAsk); -bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy); +ML_Thms.bind_thm ("Alloc_Increasing_0", Alloc_Increasing_0); +ML_Thms.bind_thm ("Alloc_Safety", Alloc_Safety); +ML_Thms.bind_thm ("Alloc_Progress", Alloc_Progress); +ML_Thms.bind_thm ("Alloc_AllowedActs", Alloc_AllowedActs); +ML_Thms.bind_thm ("Alloc_preserves_allocRel", Alloc_preserves_allocRel); +ML_Thms.bind_thm ("Alloc_preserves_allocAsk", Alloc_preserves_allocAsk); +ML_Thms.bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy); *} text{*Strip off the INT in the guarantees postcondition*} @@ -808,7 +808,7 @@ ML {* -bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing}) +ML_Thms.bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing}) *} declare System_Increasing' [intro!] diff -r 21dd034523e5 -r 8e8d28ed7529 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Tue Mar 18 10:00:23 2014 +0100 +++ b/src/Pure/ML/ml_context.ML Tue Mar 18 11:07:47 2014 +0100 @@ -4,25 +4,14 @@ ML context and antiquotations. *) -signature BASIC_ML_CONTEXT = -sig - val bind_thm: string * thm -> unit - val bind_thms: string * thm list -> unit -end - signature ML_CONTEXT = sig - include BASIC_ML_CONTEXT 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 - val ml_store_thms: string * thm list -> unit - val ml_store_thm: string * thm -> unit val check_antiquotation: Proof.context -> xstring * Position.T -> string val print_antiquotations: Proof.context -> unit type decl = Proof.context -> string * string @@ -59,41 +48,6 @@ | NONE => error "Missing context after execution"); -(* theorem bindings *) - -structure Stored_Thms = Theory_Data -( - type T = thm list; - val empty = []; - fun extend _ = []; - fun merge _ = []; -); - -fun get_stored_thms () = Stored_Thms.get (the_global_context ()); -val get_stored_thm = hd o get_stored_thms; - -fun ml_store get (name, ths) = - let - val ths' = Context.>>> (Context.map_theory_result - (Global_Theory.store_thms (Binding.name name, ths))); - val _ = Theory.setup (Stored_Thms.put ths'); - val _ = - if name = "" then () - else if not (ML_Syntax.is_identifier name) then - error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value") - else - ML_Compiler.eval true Position.none - (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();")); - val _ = Theory.setup (Stored_Thms.put []); - in () end; - -val ml_store_thms = ml_store "ML_Context.get_stored_thms"; -fun ml_store_thm (name, th) = ml_store "ML_Context.get_stored_thm" (name, [th]); - -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); - - (** ML antiquotations **) @@ -238,5 +192,3 @@ end; -structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context; -open Basic_ML_Context; diff -r 21dd034523e5 -r 8e8d28ed7529 src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Tue Mar 18 10:00:23 2014 +0100 +++ b/src/Pure/ML/ml_thms.ML Tue Mar 18 11:07:47 2014 +0100 @@ -8,6 +8,12 @@ sig val the_attributes: Proof.context -> int -> Args.src list val the_thmss: Proof.context -> thm list list + val get_stored_thms: unit -> thm list + val get_stored_thm: unit -> thm + val store_thms: string * thm list -> unit + val store_thm: string * thm -> unit + val bind_thm: string * thm -> unit + val bind_thms: string * thm list -> unit end; structure ML_Thms: ML_THMS = @@ -100,5 +106,40 @@ (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN))); in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end)); + +(* old-style theorem bindings *) + +structure Stored_Thms = Theory_Data +( + type T = thm list; + val empty = []; + fun extend _ = []; + fun merge _ = []; +); + +fun get_stored_thms () = Stored_Thms.get (ML_Context.the_global_context ()); +val get_stored_thm = hd o get_stored_thms; + +fun ml_store get (name, ths) = + let + val ths' = Context.>>> (Context.map_theory_result + (Global_Theory.store_thms (Binding.name name, ths))); + val _ = Theory.setup (Stored_Thms.put ths'); + val _ = + if name = "" then () + else if not (ML_Syntax.is_identifier name) then + error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value") + else + ML_Compiler.eval true Position.none + (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();")); + val _ = Theory.setup (Stored_Thms.put []); + in () end; + +val store_thms = ml_store "ML_Thms.get_stored_thms"; +fun store_thm (name, th) = ml_store "ML_Thms.get_stored_thm" (name, [th]); + +fun bind_thm (name, thm) = store_thm (name, Drule.export_without_context thm); +fun bind_thms (name, thms) = store_thms (name, map Drule.export_without_context thms); + end; diff -r 21dd034523e5 -r 8e8d28ed7529 src/Sequents/Washing.thy --- a/src/Sequents/Washing.thy Tue Mar 18 10:00:23 2014 +0100 +++ b/src/Sequents/Washing.thy Tue Mar 18 11:07:47 2014 +0100 @@ -32,10 +32,10 @@ (* "activate" definitions for use in proof *) -ML {* bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}]))) *} -ML {* bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}]))) *} -ML {* bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}]))) *} -ML {* bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}]))) *} +ML {* ML_Thms.bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}]))) *} +ML {* ML_Thms.bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}]))) *} +ML {* ML_Thms.bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}]))) *} +ML {* ML_Thms.bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}]))) *} (* a load of dirty clothes and two dollars gives you clean clothes *)