proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);

--- a/src/CCL/Type.thy	Wed Sep 17 21:27:34 2008 +0200
+++ b/src/CCL/Type.thy	Wed Sep 17 21:27:36 2008 +0200
@@ -137,9 +137,11 @@
                          (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE'
                                     etac bspec )),
                          (safe_tac (local_claset_of ctxt addSIs prems))])
+end
+*}
 
-  val ncanT_tac = mk_ncanT_tac @{context} [] case_rls case_rls
-end
+ML {*
+  val ncanT_tac = mk_ncanT_tac @{context} [] @{thms case_rls} @{thms case_rls}
 *}
 
 ML {*
@@ -275,8 +277,10 @@
 lemmas icanTs = zeroT succT nilT consT
 
 ML {*
-val incanT_tac = mk_ncanT_tac @{context} [] (thms "icase_rls") (thms "case_rls");
+val incanT_tac = mk_ncanT_tac @{context} [] @{thms icase_rls} @{thms case_rls};
+*}
 
+ML {*
 bind_thm ("ncaseT", incanT_tac
   "[| n:Nat; n=zero ==> b:C(zero); !!x.[| x:Nat;  n=succ(x) |] ==> c(x):C(succ(x)) |] ==> ncase(n,b,c) : C(n)");
 

--- a/src/CCL/ex/Flag.thy	Wed Sep 17 21:27:34 2008 +0200
+++ b/src/CCL/ex/Flag.thy	Wed Sep 17 21:27:36 2008 +0200
@@ -57,7 +57,7 @@
 
 ML {*
 bind_thm ("ccaseT", mk_ncanT_tac @{context}
-  (thms "flag_defs") (thms "case_rls") (thms "case_rls")
+  @{thms flag_defs} @{thms case_rls} @{thms case_rls}
   "[| c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |] ==> ccase(c,r,w,b) : C(c)");
 *}