1.1 --- a/src/HOL/Bali/WellType.thy	Wed Jul 11 11:14:51 2007 +0200
     1.2 +++ b/src/HOL/Bali/WellType.thy	Wed Jul 11 11:16:34 2007 +0200
     1.3 @@ -246,7 +246,7 @@
     1.4    "tys"   <= (type) "ty + ty list"
     1.5  
     1.6  
     1.7 -inductive2 
     1.8 +inductive
     1.9    wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
    1.10    and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
    1.11    and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
    1.12 @@ -456,7 +456,7 @@
    1.13  change_simpset (fn ss => ss delloop "split_all_tac")
    1.14  *}
    1.15  
    1.16 -inductive_cases2 wt_elim_cases [cases set]:
    1.17 +inductive_cases wt_elim_cases [cases set]:
    1.18  	"E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
    1.19  	"E,dt\<Turnstile>In2  ({accC,statDeclC,s}e..fn)\<Colon>T"
    1.20  	"E,dt\<Turnstile>In2  (e.[i])                 \<Colon>T"