--- 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
--- 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
--- 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
--- 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}
--- 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
--- 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]
--- 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!]
--- 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\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
--- 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
--- 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 \<Rightarrow> bool"
where "is_stmt t = (\<exists>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]
--- 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!]
--- 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;
--- 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;
--- 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 *)