tuned signature -- rearranged modules;
authorwenzelm
Tue Mar 18 11:07:47 2014 +0100 (2014-03-18)
changeset 561998e8d28ed7529
parent 56198 21dd034523e5
child 56200 1f9951be72b5
tuned signature -- rearranged modules;
src/CCL/CCL.thy
src/CCL/Term.thy
src/CCL/Type.thy
src/Doc/IsarImplementation/ML.thy
src/FOLP/IFOLP.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/Term.thy
src/HOL/UNITY/Comp/Alloc.thy
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_thms.ML
src/Sequents/Washing.thy
     1.1 --- a/src/CCL/CCL.thy	Tue Mar 18 10:00:23 2014 +0100
     1.2 +++ b/src/CCL/CCL.thy	Tue Mar 18 11:07:47 2014 +0100
     1.3 @@ -295,9 +295,9 @@
     1.4  val XH_to_Ds = map XH_to_D
     1.5  val XH_to_Es = map XH_to_E;
     1.6  
     1.7 -bind_thms ("ccl_rews", @{thms caseBs} @ @{thms ccl_injs} @ ccl_dstncts);
     1.8 -bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [@{thm notE}]);
     1.9 -bind_thms ("ccl_injDs", XH_to_Ds @{thms ccl_injs});
    1.10 +ML_Thms.bind_thms ("ccl_rews", @{thms caseBs} @ @{thms ccl_injs} @ ccl_dstncts);
    1.11 +ML_Thms.bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [@{thm notE}]);
    1.12 +ML_Thms.bind_thms ("ccl_injDs", XH_to_Ds @{thms ccl_injs});
    1.13  *}
    1.14  
    1.15  lemmas [simp] = ccl_rews
     2.1 --- a/src/CCL/Term.thy	Tue Mar 18 10:00:23 2014 +0100
     2.2 +++ b/src/CCL/Term.thy	Tue Mar 18 11:07:47 2014 +0100
     2.3 @@ -286,7 +286,7 @@
     2.4  subsection {* Constructors are distinct *}
     2.5  
     2.6  ML {*
     2.7 -bind_thms ("term_dstncts",
     2.8 +ML_Thms.bind_thms ("term_dstncts",
     2.9    mkall_dstnct_thms @{context} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs})
    2.10      [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
    2.11  *}
    2.12 @@ -305,7 +305,7 @@
    2.13  subsection {* Rewriting and Proving *}
    2.14  
    2.15  ML {*
    2.16 -  bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
    2.17 +  ML_Thms.bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
    2.18  *}
    2.19  
    2.20  lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews
     3.1 --- a/src/CCL/Type.thy	Tue Mar 18 10:00:23 2014 +0100
     3.2 +++ b/src/CCL/Type.thy	Tue Mar 18 11:07:47 2014 +0100
     3.3 @@ -101,7 +101,7 @@
     3.4    unfolding simp_type_defs by blast+
     3.5  
     3.6  ML {*
     3.7 -bind_thms ("case_rls", XH_to_Es @{thms XHs});
     3.8 +ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs});
     3.9  *}
    3.10  
    3.11  
    3.12 @@ -262,7 +262,7 @@
    3.13  
    3.14  lemmas iXHs = NatXH ListXH
    3.15  
    3.16 -ML {* bind_thms ("icase_rls", XH_to_Es @{thms iXHs}) *}
    3.17 +ML {* ML_Thms.bind_thms ("icase_rls", XH_to_Es @{thms iXHs}) *}
    3.18  
    3.19  
    3.20  subsection {* Type Rules *}
    3.21 @@ -340,7 +340,7 @@
    3.22  (*         - intro rules are type rules for canonical terms                *)
    3.23  (*         - elim rules are case rules (no non-canonical terms appear)     *)
    3.24  
    3.25 -ML {* bind_thms ("XHEs", XH_to_Es @{thms XHs}) *}
    3.26 +ML {* ML_Thms.bind_thms ("XHEs", XH_to_Es @{thms XHs}) *}
    3.27  
    3.28  lemmas [intro!] = SubtypeI canTs icanTs
    3.29    and [elim!] = SubtypeE XHEs
     4.1 --- a/src/Doc/IsarImplementation/ML.thy	Tue Mar 18 10:00:23 2014 +0100
     4.2 +++ b/src/Doc/IsarImplementation/ML.thy	Tue Mar 18 11:07:47 2014 +0100
     4.3 @@ -627,8 +627,8 @@
     4.4    \begin{mldecls}
     4.5    @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
     4.6    @{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\
     4.7 -  @{index_ML bind_thms: "string * thm list -> unit"} \\
     4.8 -  @{index_ML bind_thm: "string * thm -> unit"} \\
     4.9 +  @{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\
    4.10 +  @{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\
    4.11    \end{mldecls}
    4.12  
    4.13    \begin{description}
    4.14 @@ -642,12 +642,12 @@
    4.15    \item @{ML "Context.>>"}~@{text f} applies context transformation
    4.16    @{text f} to the implicit context of the ML toplevel.
    4.17  
    4.18 -  \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
    4.19 +  \item @{ML ML_Thms.bind_thms}~@{text "(name, thms)"} stores a list of
    4.20    theorems produced in ML both in the (global) theory context and the
    4.21    ML toplevel, associating it with the provided name.  Theorems are
    4.22    put into a global ``standard'' format before being stored.
    4.23  
    4.24 -  \item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a
    4.25 +  \item @{ML ML_Thms.bind_thm} is similar to @{ML ML_Thms.bind_thms} but refers to a
    4.26    singleton fact.
    4.27  
    4.28    \end{description}
     5.1 --- a/src/FOLP/IFOLP.thy	Tue Mar 18 10:00:23 2014 +0100
     5.2 +++ b/src/FOLP/IFOLP.thy	Tue Mar 18 11:07:47 2014 +0100
     5.3 @@ -411,7 +411,7 @@
     5.4    done
     5.5  
     5.6  (*NOT PROVED
     5.7 -bind_thm ("ex1_cong", prove_goal (the_context ())
     5.8 +ML_Thms.bind_thm ("ex1_cong", prove_goal (the_context ())
     5.9      "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))"
    5.10   (fn prems =>
    5.11    [ (REPEAT   (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
     6.1 --- a/src/HOL/Bali/AxSem.thy	Tue Mar 18 10:00:23 2014 +0100
     6.2 +++ b/src/HOL/Bali/AxSem.thy	Tue Mar 18 11:07:47 2014 +0100
     6.3 @@ -1006,7 +1006,7 @@
     6.4  apply  (auto simp add: type_ok_def)
     6.5  done
     6.6  
     6.7 -ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt}) *}
     6.8 +ML {* ML_Thms.bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt}) *}
     6.9  declare ax_Abrupts [intro!]
    6.10  
    6.11  lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]
     7.1 --- a/src/HOL/Bali/Eval.thy	Tue Mar 18 10:00:23 2014 +0100
     7.2 +++ b/src/HOL/Bali/Eval.thy	Tue Mar 18 11:07:47 2014 +0100
     7.3 @@ -745,7 +745,7 @@
     7.4  *)
     7.5  
     7.6  ML {*
     7.7 -bind_thm ("eval_induct", rearrange_prems 
     7.8 +ML_Thms.bind_thm ("eval_induct", rearrange_prems 
     7.9  [0,1,2,8,4,30,31,27,15,16,
    7.10   17,18,19,20,21,3,5,25,26,23,6,
    7.11   7,11,9,13,14,12,22,10,28,
    7.12 @@ -881,7 +881,7 @@
    7.13      | _ => SOME (mk_meta_eq @{thm eval_stmt_eq})) *}
    7.14  
    7.15  ML {*
    7.16 -bind_thms ("AbruptIs", sum3_instantiate @{context} @{thm eval.Abrupt})
    7.17 +ML_Thms.bind_thms ("AbruptIs", sum3_instantiate @{context} @{thm eval.Abrupt})
    7.18  *}
    7.19  
    7.20  declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!]
     8.1 --- a/src/HOL/Bali/Evaln.thy	Tue Mar 18 10:00:23 2014 +0100
     8.2 +++ b/src/HOL/Bali/Evaln.thy	Tue Mar 18 11:07:47 2014 +0100
     8.3 @@ -292,7 +292,7 @@
     8.4        (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
     8.5      | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
     8.6  
     8.7 -ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *}
     8.8 +ML {* ML_Thms.bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *}
     8.9  declare evaln_AbruptIs [intro!]
    8.10  
    8.11  lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
     9.1 --- a/src/HOL/Bali/Example.thy	Tue Mar 18 10:00:23 2014 +0100
     9.2 +++ b/src/HOL/Bali/Example.thy	Tue Mar 18 11:07:47 2014 +0100
     9.3 @@ -894,7 +894,7 @@
     9.4  
     9.5  declare member_is_static_simp [simp]
     9.6  declare wt.Skip [rule del] wt.Init [rule del]
     9.7 -ML {* bind_thms ("wt_intros", map (rewrite_rule @{context} @{thms id_def}) @{thms wt.intros}) *}
     9.8 +ML {* ML_Thms.bind_thms ("wt_intros", map (rewrite_rule @{context} @{thms id_def}) @{thms wt.intros}) *}
     9.9  lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
    9.10  lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
    9.11  
    9.12 @@ -1187,7 +1187,7 @@
    9.13  declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
    9.14          Base_foo_defs  [simp]
    9.15  
    9.16 -ML {* bind_thms ("eval_intros", map 
    9.17 +ML {* ML_Thms.bind_thms ("eval_intros", map 
    9.18          (simplify (@{context} delsimps @{thms Skip_eq} addsimps @{thms lvar_def}) o 
    9.19           rewrite_rule @{context} [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
    9.20  lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
    10.1 --- a/src/HOL/Bali/Term.thy	Tue Mar 18 10:00:23 2014 +0100
    10.2 +++ b/src/HOL/Bali/Term.thy	Tue Mar 18 11:07:47 2014 +0100
    10.3 @@ -262,7 +262,7 @@
    10.4    is_stmt :: "term \<Rightarrow> bool"
    10.5    where "is_stmt t = (\<exists>c. t=In1r c)"
    10.6  
    10.7 -ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *}
    10.8 +ML {* ML_Thms.bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *}
    10.9  
   10.10  declare is_stmt_rews [simp]
   10.11  
    11.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Tue Mar 18 10:00:23 2014 +0100
    11.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Tue Mar 18 11:07:47 2014 +0100
    11.3 @@ -425,7 +425,7 @@
    11.4    apply (rule fst_o_funPair)
    11.5    done
    11.6  
    11.7 -ML {* bind_thms ("fst_o_client_map'", make_o_equivs @{context} @{thm fst_o_client_map}) *}
    11.8 +ML {* ML_Thms.bind_thms ("fst_o_client_map'", make_o_equivs @{context} @{thm fst_o_client_map}) *}
    11.9  declare fst_o_client_map' [simp]
   11.10  
   11.11  lemma snd_o_client_map: "snd o client_map = clientState_d.dummy"
   11.12 @@ -433,7 +433,7 @@
   11.13    apply (rule snd_o_funPair)
   11.14    done
   11.15  
   11.16 -ML {* bind_thms ("snd_o_client_map'", make_o_equivs @{context} @{thm snd_o_client_map}) *}
   11.17 +ML {* ML_Thms.bind_thms ("snd_o_client_map'", make_o_equivs @{context} @{thm snd_o_client_map}) *}
   11.18  declare snd_o_client_map' [simp]
   11.19  
   11.20  
   11.21 @@ -443,28 +443,28 @@
   11.22    apply record_auto
   11.23    done
   11.24  
   11.25 -ML {* bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{context} @{thm client_o_sysOfAlloc}) *}
   11.26 +ML {* ML_Thms.bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{context} @{thm client_o_sysOfAlloc}) *}
   11.27  declare client_o_sysOfAlloc' [simp]
   11.28  
   11.29  lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv"
   11.30    apply record_auto
   11.31    done
   11.32  
   11.33 -ML {* bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfAlloc_eq}) *}
   11.34 +ML {* ML_Thms.bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfAlloc_eq}) *}
   11.35  declare allocGiv_o_sysOfAlloc_eq' [simp]
   11.36  
   11.37  lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk"
   11.38    apply record_auto
   11.39    done
   11.40  
   11.41 -ML {* bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfAlloc_eq}) *}
   11.42 +ML {* ML_Thms.bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfAlloc_eq}) *}
   11.43  declare allocAsk_o_sysOfAlloc_eq' [simp]
   11.44  
   11.45  lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel"
   11.46    apply record_auto
   11.47    done
   11.48  
   11.49 -ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfAlloc_eq}) *}
   11.50 +ML {* ML_Thms.bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfAlloc_eq}) *}
   11.51  declare allocRel_o_sysOfAlloc_eq' [simp]
   11.52  
   11.53  
   11.54 @@ -474,49 +474,49 @@
   11.55    apply record_auto
   11.56    done
   11.57  
   11.58 -ML {* bind_thms ("client_o_sysOfClient'", make_o_equivs @{context} @{thm client_o_sysOfClient}) *}
   11.59 +ML {* ML_Thms.bind_thms ("client_o_sysOfClient'", make_o_equivs @{context} @{thm client_o_sysOfClient}) *}
   11.60  declare client_o_sysOfClient' [simp]
   11.61  
   11.62  lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd "
   11.63    apply record_auto
   11.64    done
   11.65  
   11.66 -ML {* bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfClient_eq}) *}
   11.67 +ML {* ML_Thms.bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfClient_eq}) *}
   11.68  declare allocGiv_o_sysOfClient_eq' [simp]
   11.69  
   11.70  lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd "
   11.71    apply record_auto
   11.72    done
   11.73  
   11.74 -ML {* bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfClient_eq}) *}
   11.75 +ML {* ML_Thms.bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfClient_eq}) *}
   11.76  declare allocAsk_o_sysOfClient_eq' [simp]
   11.77  
   11.78  lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd "
   11.79    apply record_auto
   11.80    done
   11.81  
   11.82 -ML {* bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfClient_eq}) *}
   11.83 +ML {* ML_Thms.bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfClient_eq}) *}
   11.84  declare allocRel_o_sysOfClient_eq' [simp]
   11.85  
   11.86  lemma allocGiv_o_inv_sysOfAlloc_eq: "allocGiv o inv sysOfAlloc = allocGiv"
   11.87    apply (simp add: o_def)
   11.88    done
   11.89  
   11.90 -ML {* bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_inv_sysOfAlloc_eq}) *}
   11.91 +ML {* ML_Thms.bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_inv_sysOfAlloc_eq}) *}
   11.92  declare allocGiv_o_inv_sysOfAlloc_eq' [simp]
   11.93  
   11.94  lemma allocAsk_o_inv_sysOfAlloc_eq: "allocAsk o inv sysOfAlloc = allocAsk"
   11.95    apply (simp add: o_def)
   11.96    done
   11.97  
   11.98 -ML {* bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_inv_sysOfAlloc_eq}) *}
   11.99 +ML {* ML_Thms.bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_inv_sysOfAlloc_eq}) *}
  11.100  declare allocAsk_o_inv_sysOfAlloc_eq' [simp]
  11.101  
  11.102  lemma allocRel_o_inv_sysOfAlloc_eq: "allocRel o inv sysOfAlloc = allocRel"
  11.103    apply (simp add: o_def)
  11.104    done
  11.105  
  11.106 -ML {* bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_inv_sysOfAlloc_eq}) *}
  11.107 +ML {* ML_Thms.bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_inv_sysOfAlloc_eq}) *}
  11.108  declare allocRel_o_inv_sysOfAlloc_eq' [simp]
  11.109  
  11.110  lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) =
  11.111 @@ -524,7 +524,7 @@
  11.112    apply (simp add: o_def drop_map_def)
  11.113    done
  11.114  
  11.115 -ML {* bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{context} @{thm rel_inv_client_map_drop_map}) *}
  11.116 +ML {* ML_Thms.bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{context} @{thm rel_inv_client_map_drop_map}) *}
  11.117  declare rel_inv_client_map_drop_map [simp]
  11.118  
  11.119  lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) =
  11.120 @@ -532,7 +532,7 @@
  11.121    apply (simp add: o_def drop_map_def)
  11.122    done
  11.123  
  11.124 -ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{context} @{thm ask_inv_client_map_drop_map}) *}
  11.125 +ML {* ML_Thms.bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{context} @{thm ask_inv_client_map_drop_map}) *}
  11.126  declare ask_inv_client_map_drop_map [simp]
  11.127  
  11.128  
  11.129 @@ -549,13 +549,13 @@
  11.130          @{thm Client} |> simplify (@{context} addsimps @{thms client_spec_simps})
  11.131                 |> list_of_Int;
  11.132  
  11.133 -bind_thm ("Client_Increasing_ask", Client_Increasing_ask);
  11.134 -bind_thm ("Client_Increasing_rel", Client_Increasing_rel);
  11.135 -bind_thm ("Client_Bounded", Client_Bounded);
  11.136 -bind_thm ("Client_Progress", Client_Progress);
  11.137 -bind_thm ("Client_AllowedActs", Client_AllowedActs);
  11.138 -bind_thm ("Client_preserves_giv", Client_preserves_giv);
  11.139 -bind_thm ("Client_preserves_dummy", Client_preserves_dummy);
  11.140 +ML_Thms.bind_thm ("Client_Increasing_ask", Client_Increasing_ask);
  11.141 +ML_Thms.bind_thm ("Client_Increasing_rel", Client_Increasing_rel);
  11.142 +ML_Thms.bind_thm ("Client_Bounded", Client_Bounded);
  11.143 +ML_Thms.bind_thm ("Client_Progress", Client_Progress);
  11.144 +ML_Thms.bind_thm ("Client_AllowedActs", Client_AllowedActs);
  11.145 +ML_Thms.bind_thm ("Client_preserves_giv", Client_preserves_giv);
  11.146 +ML_Thms.bind_thm ("Client_preserves_dummy", Client_preserves_dummy);
  11.147  *}
  11.148  
  11.149  declare
  11.150 @@ -579,13 +579,13 @@
  11.151          @{thm Network} |> simplify (@{context} addsimps @{thms network_spec_simps})
  11.152                  |> list_of_Int;
  11.153  
  11.154 -bind_thm ("Network_Ask", Network_Ask);
  11.155 -bind_thm ("Network_Giv", Network_Giv);
  11.156 -bind_thm ("Network_Rel", Network_Rel);
  11.157 -bind_thm ("Network_AllowedActs", Network_AllowedActs);
  11.158 -bind_thm ("Network_preserves_allocGiv", Network_preserves_allocGiv);
  11.159 -bind_thm ("Network_preserves_rel", Network_preserves_rel);
  11.160 -bind_thm ("Network_preserves_ask", Network_preserves_ask);
  11.161 +ML_Thms.bind_thm ("Network_Ask", Network_Ask);
  11.162 +ML_Thms.bind_thm ("Network_Giv", Network_Giv);
  11.163 +ML_Thms.bind_thm ("Network_Rel", Network_Rel);
  11.164 +ML_Thms.bind_thm ("Network_AllowedActs", Network_AllowedActs);
  11.165 +ML_Thms.bind_thm ("Network_preserves_allocGiv", Network_preserves_allocGiv);
  11.166 +ML_Thms.bind_thm ("Network_preserves_rel", Network_preserves_rel);
  11.167 +ML_Thms.bind_thm ("Network_preserves_ask", Network_preserves_ask);
  11.168  *}
  11.169  
  11.170  declare Network_preserves_allocGiv [iff]
  11.171 @@ -610,13 +610,13 @@
  11.172          @{thm Alloc} |> simplify (@{context} addsimps @{thms alloc_spec_simps})
  11.173                |> list_of_Int;
  11.174  
  11.175 -bind_thm ("Alloc_Increasing_0", Alloc_Increasing_0);
  11.176 -bind_thm ("Alloc_Safety", Alloc_Safety);
  11.177 -bind_thm ("Alloc_Progress", Alloc_Progress);
  11.178 -bind_thm ("Alloc_AllowedActs", Alloc_AllowedActs);
  11.179 -bind_thm ("Alloc_preserves_allocRel", Alloc_preserves_allocRel);
  11.180 -bind_thm ("Alloc_preserves_allocAsk", Alloc_preserves_allocAsk);
  11.181 -bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy);
  11.182 +ML_Thms.bind_thm ("Alloc_Increasing_0", Alloc_Increasing_0);
  11.183 +ML_Thms.bind_thm ("Alloc_Safety", Alloc_Safety);
  11.184 +ML_Thms.bind_thm ("Alloc_Progress", Alloc_Progress);
  11.185 +ML_Thms.bind_thm ("Alloc_AllowedActs", Alloc_AllowedActs);
  11.186 +ML_Thms.bind_thm ("Alloc_preserves_allocRel", Alloc_preserves_allocRel);
  11.187 +ML_Thms.bind_thm ("Alloc_preserves_allocAsk", Alloc_preserves_allocAsk);
  11.188 +ML_Thms.bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy);
  11.189  *}
  11.190  
  11.191  text{*Strip off the INT in the guarantees postcondition*}
  11.192 @@ -808,7 +808,7 @@
  11.193  
  11.194  
  11.195  ML {*
  11.196 -bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing})
  11.197 +ML_Thms.bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing})
  11.198  *}
  11.199  
  11.200  declare System_Increasing' [intro!]
    12.1 --- a/src/Pure/ML/ml_context.ML	Tue Mar 18 10:00:23 2014 +0100
    12.2 +++ b/src/Pure/ML/ml_context.ML	Tue Mar 18 11:07:47 2014 +0100
    12.3 @@ -4,25 +4,14 @@
    12.4  ML context and antiquotations.
    12.5  *)
    12.6  
    12.7 -signature BASIC_ML_CONTEXT =
    12.8 -sig
    12.9 -  val bind_thm: string * thm -> unit
   12.10 -  val bind_thms: string * thm list -> unit
   12.11 -end
   12.12 -
   12.13  signature ML_CONTEXT =
   12.14  sig
   12.15 -  include BASIC_ML_CONTEXT
   12.16    val the_generic_context: unit -> Context.generic
   12.17    val the_global_context: unit -> theory
   12.18    val the_local_context: unit -> Proof.context
   12.19    val thm: xstring -> thm
   12.20    val thms: xstring -> thm list
   12.21    val exec: (unit -> unit) -> Context.generic -> Context.generic
   12.22 -  val get_stored_thms: unit -> thm list
   12.23 -  val get_stored_thm: unit -> thm
   12.24 -  val ml_store_thms: string * thm list -> unit
   12.25 -  val ml_store_thm: string * thm -> unit
   12.26    val check_antiquotation: Proof.context -> xstring * Position.T -> string
   12.27    val print_antiquotations: Proof.context -> unit
   12.28    type decl = Proof.context -> string * string
   12.29 @@ -59,41 +48,6 @@
   12.30    | NONE => error "Missing context after execution");
   12.31  
   12.32  
   12.33 -(* theorem bindings *)
   12.34 -
   12.35 -structure Stored_Thms = Theory_Data
   12.36 -(
   12.37 -  type T = thm list;
   12.38 -  val empty = [];
   12.39 -  fun extend _ = [];
   12.40 -  fun merge _ = [];
   12.41 -);
   12.42 -
   12.43 -fun get_stored_thms () = Stored_Thms.get (the_global_context ());
   12.44 -val get_stored_thm = hd o get_stored_thms;
   12.45 -
   12.46 -fun ml_store get (name, ths) =
   12.47 -  let
   12.48 -    val ths' = Context.>>> (Context.map_theory_result
   12.49 -      (Global_Theory.store_thms (Binding.name name, ths)));
   12.50 -    val _ = Theory.setup (Stored_Thms.put ths');
   12.51 -    val _ =
   12.52 -      if name = "" then ()
   12.53 -      else if not (ML_Syntax.is_identifier name) then
   12.54 -        error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
   12.55 -      else
   12.56 -        ML_Compiler.eval true Position.none
   12.57 -          (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
   12.58 -    val _ = Theory.setup (Stored_Thms.put []);
   12.59 -  in () end;
   12.60 -
   12.61 -val ml_store_thms = ml_store "ML_Context.get_stored_thms";
   12.62 -fun ml_store_thm (name, th) = ml_store "ML_Context.get_stored_thm" (name, [th]);
   12.63 -
   12.64 -fun bind_thm (name, thm) = ml_store_thm (name, Drule.export_without_context thm);
   12.65 -fun bind_thms (name, thms) = ml_store_thms (name, map Drule.export_without_context thms);
   12.66 -
   12.67 -
   12.68  
   12.69  (** ML antiquotations **)
   12.70  
   12.71 @@ -238,5 +192,3 @@
   12.72  
   12.73  end;
   12.74  
   12.75 -structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context;
   12.76 -open Basic_ML_Context;
    13.1 --- a/src/Pure/ML/ml_thms.ML	Tue Mar 18 10:00:23 2014 +0100
    13.2 +++ b/src/Pure/ML/ml_thms.ML	Tue Mar 18 11:07:47 2014 +0100
    13.3 @@ -8,6 +8,12 @@
    13.4  sig
    13.5    val the_attributes: Proof.context -> int -> Args.src list
    13.6    val the_thmss: Proof.context -> thm list list
    13.7 +  val get_stored_thms: unit -> thm list
    13.8 +  val get_stored_thm: unit -> thm
    13.9 +  val store_thms: string * thm list -> unit
   13.10 +  val store_thm: string * thm -> unit
   13.11 +  val bind_thm: string * thm -> unit
   13.12 +  val bind_thms: string * thm list -> unit
   13.13  end;
   13.14  
   13.15  structure ML_Thms: ML_THMS =
   13.16 @@ -100,5 +106,40 @@
   13.17              (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
   13.18        in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end));
   13.19  
   13.20 +
   13.21 +(* old-style theorem bindings *)
   13.22 +
   13.23 +structure Stored_Thms = Theory_Data
   13.24 +(
   13.25 +  type T = thm list;
   13.26 +  val empty = [];
   13.27 +  fun extend _ = [];
   13.28 +  fun merge _ = [];
   13.29 +);
   13.30 +
   13.31 +fun get_stored_thms () = Stored_Thms.get (ML_Context.the_global_context ());
   13.32 +val get_stored_thm = hd o get_stored_thms;
   13.33 +
   13.34 +fun ml_store get (name, ths) =
   13.35 +  let
   13.36 +    val ths' = Context.>>> (Context.map_theory_result
   13.37 +      (Global_Theory.store_thms (Binding.name name, ths)));
   13.38 +    val _ = Theory.setup (Stored_Thms.put ths');
   13.39 +    val _ =
   13.40 +      if name = "" then ()
   13.41 +      else if not (ML_Syntax.is_identifier name) then
   13.42 +        error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
   13.43 +      else
   13.44 +        ML_Compiler.eval true Position.none
   13.45 +          (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
   13.46 +    val _ = Theory.setup (Stored_Thms.put []);
   13.47 +  in () end;
   13.48 +
   13.49 +val store_thms = ml_store "ML_Thms.get_stored_thms";
   13.50 +fun store_thm (name, th) = ml_store "ML_Thms.get_stored_thm" (name, [th]);
   13.51 +
   13.52 +fun bind_thm (name, thm) = store_thm (name, Drule.export_without_context thm);
   13.53 +fun bind_thms (name, thms) = store_thms (name, map Drule.export_without_context thms);
   13.54 +
   13.55  end;
   13.56  
    14.1 --- a/src/Sequents/Washing.thy	Tue Mar 18 10:00:23 2014 +0100
    14.2 +++ b/src/Sequents/Washing.thy	Tue Mar 18 11:07:47 2014 +0100
    14.3 @@ -32,10 +32,10 @@
    14.4  
    14.5  (* "activate" definitions for use in proof *)
    14.6  
    14.7 -ML {* bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}]))) *}
    14.8 -ML {* bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}]))) *}
    14.9 -ML {* bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}]))) *}
   14.10 -ML {* bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}]))) *}
   14.11 +ML {* ML_Thms.bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}]))) *}
   14.12 +ML {* ML_Thms.bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}]))) *}
   14.13 +ML {* ML_Thms.bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}]))) *}
   14.14 +ML {* ML_Thms.bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}]))) *}
   14.15  
   14.16  (* a load of dirty clothes and two dollars gives you clean clothes *)
   14.17