src/CCL/Type.thy

--- 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)");