src/HOL/Bali/Eval.thy
changeset 61989 ba8c284d4725
parent 59498 50b60f501b05
child 62042 6c6ccf573479
--- a/src/HOL/Bali/Eval.thy	Wed Dec 30 19:41:48 2015 +0100
+++ b/src/HOL/Bali/Eval.thy	Wed Dec 30 19:57:37 2015 +0100
@@ -124,7 +124,7 @@
  assignment. 
 *}
 
-abbreviation (xsymbols)
+abbreviation
   dummy_res :: "vals" ("\<diamondsuit>")
   where "\<diamondsuit> == In1 Unit"