1.1 --- a/src/HOL/Bali/WellType.thy	Mon Jun 16 17:56:08 2008 +0200
     1.2 +++ b/src/HOL/Bali/WellType.thy	Mon Jun 16 22:13:39 2008 +0200
     1.3 @@ -653,10 +653,11 @@
     1.4  apply (safe del: disjE)
     1.5  (* 17 subgoals *)
     1.6  apply (tactic {* ALLGOALS (fn i =>
     1.7 -  if i = 11 then EVERY'[RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
     1.8 -    RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
     1.9 -    RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
    1.10 -  else RuleInsts.thin_tac @{context} "All ?P" i) *})
    1.11 +  if i = 11 then EVERY'
    1.12 +   [thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
    1.13 +    thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
    1.14 +    thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
    1.15 +  else thin_tac @{context} "All ?P" i) *})
    1.16  (*apply (safe del: disjE elim!: wt_elim_cases)*)
    1.17  apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*})
    1.18  apply (simp_all (no_asm_use) split del: split_if_asm)