diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/NanoJava/Example.thy
--- a/src/HOL/NanoJava/Example.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/NanoJava/Example.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -50,11 +50,14 @@
 consts suc  :: mname
        add  :: mname
 consts any  :: vname
-syntax dummy:: expr ("<>")
-       one  :: expr
-translations 
-      "<>"  == "LAcc any"
-      "one" == "{Nat}new Nat..suc(<>)"
+
+abbreviation
+  dummy :: expr ("<>")
+  where "<> == LAcc any"
+
+abbreviation
+  one :: expr
+  where "one == {Nat}new Nat..suc(<>)"
 
 text {* The following properties could be derived from a more complete
         program model, which we leave out for laziness. *}