--- a/src/CCL/Term.thy Mon Oct 01 12:25:04 2007 +0200
+++ b/src/CCL/Term.thy Mon Oct 01 15:14:51 2007 +0200
@@ -220,7 +220,7 @@
end
*}
-ML {*
+ML_setup {*
bind_thm ("ifBtrue", mk_beta_rl "if true then t else u = t");
bind_thm ("ifBfalse", mk_beta_rl "if false then t else u = u");
bind_thm ("ifBbot", mk_beta_rl "if bot then t else u = bot");
@@ -272,7 +272,7 @@
subsection {* Constructors are injective *}
-ML {*
+ML_setup {*
bind_thms ("term_injs", map (mk_inj_rl (the_context ())
[thm "applyB", thm "splitB", thm "whenBinl", thm "whenBinr", thm "ncaseBsucc", thm "lcaseBcons"])
@@ -285,7 +285,7 @@
subsection {* Constructors are distinct *}
-ML {*
+ML_setup {*
bind_thms ("term_dstncts",
mkall_dstnct_thms (the_context ()) (thms "data_defs") (thms "ccl_injs" @ thms "term_injs")
[["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","op $"]]);
@@ -294,7 +294,7 @@
subsection {* Rules for pre-order @{text "[="} *}
-ML {*
+ML_setup {*
local
fun mk_thm s = prove_goalw (the_context ()) (thms "data_defs") s (fn _ =>
@@ -311,8 +311,8 @@
subsection {* Rewriting and Proving *}
-ML {*
- bind_thms ("term_injDs", XH_to_Ds term_injs);
+ML_setup {*
+ bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
*}
lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews