diff -r 53716a67c3b1 -r a0e57fb1b930 src/CCL/ex/Flag.thy
--- a/src/CCL/ex/Flag.thy	Thu Jul 23 20:05:20 2009 +0200
+++ b/src/CCL/ex/Flag.thy	Thu Jul 23 21:59:56 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      CCL/ex/Flag.thy
-    ID:         $Id$
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
@@ -55,12 +54,10 @@
   and blueT: "blue : Colour"
   unfolding ColourXH by blast+
 
-ML {*
-bind_thm ("ccaseT", mk_ncanT_tac @{context}
-  @{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)");
-*}
-
+lemma ccaseT:
+  "[| c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |]
+    ==> ccase(c,r,w,b) : C(c)"
+  unfolding flag_defs by ncanT
 
 lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)"
   apply (unfold flag_def)