# HG changeset patch
# User wenzelm
# Date 1191244491 -7200
# Node ID 3be1580de4cc5d09919281248b27f5baeee00b99
# Parent  33b7fbc073613dbc8b3bd9d80b2bb5f4df89de4e
ML_setup for bind_thms;

diff -r 33b7fbc07361 -r 3be1580de4cc src/CCL/Term.thy
--- 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