diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -111,19 +111,21 @@
 
 
 abbreviation
-  NP  :: xcpt
+  NP  :: xcpt where
   "NP == NullPointer"
 
-  tprg  ::"java_mb prog"
+abbreviation
+  tprg  ::"java_mb prog" where
   "tprg == [ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]"
 
-  obj1  :: obj
+abbreviation
+  obj1  :: obj where
   "obj1 == (Ext, empty((vee, Base)\<mapsto>Bool False) ((vee, Ext )\<mapsto>Intg 0))"
 
-  "s0 == Norm    (empty, empty)"
-  "s1 == Norm    (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
-  "s2 == Norm    (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
-  "s3 == (Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
+abbreviation "s0 == Norm    (empty, empty)"
+abbreviation "s1 == Norm    (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
+abbreviation "s2 == Norm    (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
+abbreviation "s3 == (Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
 
 ML {* bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps"))) *}
 lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb"