--- a/src/HOL/IMP/Expr.thy Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/IMP/Expr.thy Tue Jun 30 20:51:15 1998 +0200
@@ -7,7 +7,7 @@
Not used in the rest of the language, but included for completeness.
*)
-Expr = Arith +
+Expr = Arith + Inductive +
(** Arithmetic expressions **)
types loc