# HG changeset patch
# User wenzelm
# Date 1390072856 -3600
# Node ID f2179be648053519321c03b8b4f4faa964fd0ee8
# Parent  74dfec1edf8cc104748b59c2ad24aa8244b08da7
prefer Isar commands over old-fashioned ML (see also a189c6274c7a);
removed pointless space: the second "_ \<Colon> _" should take precendence anyway;

diff -r 74dfec1edf8c -r f2179be64805 src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Sat Jan 18 19:46:58 2014 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Sat Jan 18 20:20:56 2014 +0100
@@ -48,33 +48,23 @@
   "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
 
 (* type constraints with spacing *)
-setup {*
-let
-  val typ = Simple_Syntax.read_typ;
-in
-  Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
-   [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
-    ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
-  Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
-   [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
-    ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
-end
-*}
+
+no_syntax (xsymbols output)
+  "_constrain" :: "logic => type => logic"  ("_\<Colon>_" [4, 0] 3)
+  "_constrain" :: "prop' => type => prop'"  ("_\<Colon>_" [4, 0] 3)
+
+syntax (xsymbols output)
+  "_constrain" :: "logic => type => logic"  ("_ \<Colon> _" [4, 0] 3)
+  "_constrain" :: "prop' => type => prop'"  ("_ \<Colon> _" [4, 0] 3)
+
 
 (* sorts as intersections *)
-setup {*
-let
-  val sortT = Type ("sort", []); (*FIXME*)
-  val classesT = Type ("classes", []); (*FIXME*)
-in
-  Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
-    ("_topsort", sortT, Mixfix ("\<top>", [], 1000)),
-    ("_sort", classesT --> sortT, Mixfix ("'(_')", [], 1000)),
-    ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], 1000)),
-    ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], 1000))
-  ]
-end
-*}
+
+syntax (xsymbols output)
+  "_topsort" :: "sort"  ("\<top>" 1000)
+  "_sort" :: "classes => sort"  ("'(_')" 1000)
+  "_classes" :: "id => classes => classes"  ("_ \<inter> _" 1000)
+  "_classes" :: "longid => classes => classes"  ("_ \<inter> _" 1000)
 
 end
 (*>*)