src/HOL/Library/OptionalSugar.thy
changeset 42293 6cca0343ea48
parent 42288 2074b31650e6
child 42297 140f283266b7
     1.1 --- a/src/HOL/Library/OptionalSugar.thy	Fri Apr 08 16:38:46 2011 +0200
     1.2 +++ b/src/HOL/Library/OptionalSugar.thy	Fri Apr 08 17:45:37 2011 +0200
     1.3 @@ -51,15 +51,13 @@
     1.4  setup {*
     1.5  let
     1.6    val typ = Simple_Syntax.read_typ;
     1.7 -  val typeT = Syntax_Ext.typeT;
     1.8 -  val spropT = Syntax_Ext.spropT;
     1.9  in
    1.10 -  Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
    1.11 -    ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    1.12 -    ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
    1.13 -  #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
    1.14 -      ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    1.15 -      ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
    1.16 +  Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
    1.17 +   [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    1.18 +    ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
    1.19 +  Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
    1.20 +   [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    1.21 +    ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
    1.22  end
    1.23  *}
    1.24