--- a/src/HOL/MicroJava/J/WellType.thy Wed Jul 11 11:29:44 2007 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy Wed Jul 11 11:32:02 2007 +0200
@@ -107,7 +107,7 @@
-- "method body with parameter names, local variables, block, result expression."
-- "local variables might include This, which is hidden anyway"
-inductive2
+inductive
ty_expr :: "'c env => expr => ty => bool" ("_ \<turnstile> _ :: _" [51, 51, 51] 50)
and ty_exprs :: "'c env => expr list => ty list => bool" ("_ \<turnstile> _ [::] _" [51, 51, 51] 50)
and wt_stmt :: "'c env => stmt => bool" ("_ \<turnstile> _ \<surd>" [51, 51] 50)