src/HOL/Bali/WellType.thy
changeset 27239 f2f42f9fa09d
parent 27208 5fe899199f85
child 30235 58d147683393
--- a/src/HOL/Bali/WellType.thy	Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Bali/WellType.thy	Mon Jun 16 22:13:39 2008 +0200
@@ -653,10 +653,11 @@
 apply (safe del: disjE)
 (* 17 subgoals *)
 apply (tactic {* ALLGOALS (fn i =>
-  if i = 11 then EVERY'[RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
-    RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
-    RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
-  else RuleInsts.thin_tac @{context} "All ?P" i) *})
+  if i = 11 then EVERY'
+   [thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
+    thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
+    thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
+  else thin_tac @{context} "All ?P" i) *})
 (*apply (safe del: disjE elim!: wt_elim_cases)*)
 apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*})
 apply (simp_all (no_asm_use) split del: split_if_asm)