src/CCL/ex/Flag.thy
changeset 27221 31328dc30196
parent 23894 1a4167d761ac
child 28272 ed959a0f650b
--- a/src/CCL/ex/Flag.thy	Sat Jun 14 23:33:43 2008 +0200
+++ b/src/CCL/ex/Flag.thy	Sat Jun 14 23:52:51 2008 +0200
@@ -64,15 +64,17 @@
 
 lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)"
   apply (unfold flag_def)
-  apply (tactic {* typechk_tac [thm "redT", thm "whiteT", thm "blueT", thm "ccaseT"] 1 *})
-  apply (tactic clean_ccs_tac)
+  apply (tactic {* typechk_tac @{context}
+    [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *})
+  apply (tactic "clean_ccs_tac @{context}")
   apply (erule ListPRI [THEN ListPR_wf [THEN wfI]])
   apply assumption
   done
 
 lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).FLAG(x,l)}"
   apply (unfold flag_def)
-  apply (tactic {* gen_ccs_tac [thm "redT", thm "whiteT", thm "blueT", thm "ccaseT"] 1 *})
+  apply (tactic {* gen_ccs_tac @{context}
+    [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *})
   oops
 
 end