diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy	Wed Feb 24 22:09:50 2010 +0100
@@ -38,24 +38,13 @@
             xconf (heap (store s)) (abrupt s)"
 
 
-syntax (xsymbols)
-  hext     :: "aheap => aheap => bool"
-              ("_ \<le>| _" [51,51] 50)
-
-  conf     :: "'c prog => aheap => val => ty => bool"
-              ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
-
-  lconf    :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
-              ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
-
-  oconf    :: "'c prog => aheap => obj => bool"
-              ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
-
-  hconf    :: "'c prog => aheap => bool"
-              ("_ \<turnstile>h _ \<surd>" [51,51] 50)
-
-  conforms :: "state => java_mb env' => bool"
-              ("_ ::\<preceq> _" [51,51] 50)
+notation (xsymbols)
+  hext  ("_ \<le>| _" [51,51] 50) and
+  conf  ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50) and
+  lconf  ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50) and
+  oconf  ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50) and
+  hconf  ("_ \<turnstile>h _ \<surd>" [51,51] 50) and
+  conforms  ("_ ::\<preceq> _" [51,51] 50)
 
 
 section "hext"