diff -r b3196458428b -r 6cca0343ea48 doc-src/Codegen/Thy/Setup.thy
--- a/doc-src/Codegen/Thy/Setup.thy	Fri Apr 08 16:38:46 2011 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy	Fri Apr 08 17:45:37 2011 +0200
@@ -10,15 +10,13 @@
 setup {*
 let
   val typ = Simple_Syntax.read_typ;
-  val typeT = Syntax_Ext.typeT;
-  val spropT = Syntax_Ext.spropT;
 in
-  Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
-    ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
-    ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
-  #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
-      ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
-      ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
+  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
 *}