src/HOL/Library/OptionalSugar.thy
changeset 42288 2074b31650e6
parent 38864 4abe644fcea5
child 42293 6cca0343ea48
     1.1 --- a/src/HOL/Library/OptionalSugar.thy	Fri Apr 08 14:20:57 2011 +0200
     1.2 +++ b/src/HOL/Library/OptionalSugar.thy	Fri Apr 08 15:02:11 2011 +0200
     1.3 @@ -51,8 +51,8 @@
     1.4  setup {*
     1.5  let
     1.6    val typ = Simple_Syntax.read_typ;
     1.7 -  val typeT = Syntax.typeT;
     1.8 -  val spropT = Syntax.spropT;
     1.9 +  val typeT = Syntax_Ext.typeT;
    1.10 +  val spropT = Syntax_Ext.spropT;
    1.11  in
    1.12    Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
    1.13      ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),