src/CCL/ex/Flag.thy
changeset 23894 1a4167d761ac
parent 20140 98acc6d0fab6
child 27221 31328dc30196
--- a/src/CCL/ex/Flag.thy	Sat Jul 21 17:40:40 2007 +0200
+++ b/src/CCL/ex/Flag.thy	Sat Jul 21 23:25:00 2007 +0200
@@ -56,7 +56,7 @@
   unfolding ColourXH by blast+
 
 ML {*
-bind_thm ("ccaseT", mk_ncanT_tac (the_context ())
+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)");
 *}