src/HOL/Library/OptionalSugar.thy
changeset 55038 f2179be64805
parent 42297 140f283266b7
child 55052 c602013f127e
     1.1 --- a/src/HOL/Library/OptionalSugar.thy	Sat Jan 18 19:46:58 2014 +0100
     1.2 +++ b/src/HOL/Library/OptionalSugar.thy	Sat Jan 18 20:20:56 2014 +0100
     1.3 @@ -48,33 +48,23 @@
     1.4    "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
     1.5  
     1.6  (* type constraints with spacing *)
     1.7 -setup {*
     1.8 -let
     1.9 -  val typ = Simple_Syntax.read_typ;
    1.10 -in
    1.11 -  Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
    1.12 -   [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    1.13 -    ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
    1.14 -  Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
    1.15 -   [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    1.16 -    ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
    1.17 -end
    1.18 -*}
    1.19 +
    1.20 +no_syntax (xsymbols output)
    1.21 +  "_constrain" :: "logic => type => logic"  ("_\<Colon>_" [4, 0] 3)
    1.22 +  "_constrain" :: "prop' => type => prop'"  ("_\<Colon>_" [4, 0] 3)
    1.23 +
    1.24 +syntax (xsymbols output)
    1.25 +  "_constrain" :: "logic => type => logic"  ("_ \<Colon> _" [4, 0] 3)
    1.26 +  "_constrain" :: "prop' => type => prop'"  ("_ \<Colon> _" [4, 0] 3)
    1.27 +
    1.28  
    1.29  (* sorts as intersections *)
    1.30 -setup {*
    1.31 -let
    1.32 -  val sortT = Type ("sort", []); (*FIXME*)
    1.33 -  val classesT = Type ("classes", []); (*FIXME*)
    1.34 -in
    1.35 -  Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
    1.36 -    ("_topsort", sortT, Mixfix ("\<top>", [], 1000)),
    1.37 -    ("_sort", classesT --> sortT, Mixfix ("'(_')", [], 1000)),
    1.38 -    ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], 1000)),
    1.39 -    ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], 1000))
    1.40 -  ]
    1.41 -end
    1.42 -*}
    1.43 +
    1.44 +syntax (xsymbols output)
    1.45 +  "_topsort" :: "sort"  ("\<top>" 1000)
    1.46 +  "_sort" :: "classes => sort"  ("'(_')" 1000)
    1.47 +  "_classes" :: "id => classes => classes"  ("_ \<inter> _" 1000)
    1.48 +  "_classes" :: "longid => classes => classes"  ("_ \<inter> _" 1000)
    1.49  
    1.50  end
    1.51  (*>*)