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