renamed sprop "prop#" to "prop'" -- proper identifier;
eliminated spurious symbolic string bindings (logic, any etc.);
hardwired special "prop" vs. "prop'" conversion;
tuned;

--- 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
 *}
 

--- a/src/HOL/Imperative_HOL/Overview.thy	Fri Apr 08 16:38:46 2011 +0200
+++ b/src/HOL/Imperative_HOL/Overview.thy	Fri Apr 08 17:45:37 2011 +0200
@@ -11,15 +11,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
 *}(*>*)
 

--- a/src/HOL/Library/OptionalSugar.thy	Fri Apr 08 16:38:46 2011 +0200
+++ b/src/HOL/Library/OptionalSugar.thy	Fri Apr 08 17:45:37 2011 +0200
@@ -51,15 +51,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
 *}
 

--- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 16:38:46 2011 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 17:45:37 2011 +0200
@@ -88,7 +88,8 @@
 
 (* syn_ext_types *)
 
-fun make_type n = replicate n Syntax_Ext.typeT ---> Syntax_Ext.typeT;
+val typeT = Type ("type", []);
+fun make_type n = replicate n typeT ---> typeT;
 
 fun syn_ext_types type_decls =
   let
@@ -150,8 +151,7 @@
       |> map (Syntax_Ext.stamp_trfun binder_stamp o
           apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
   in
-    Syntax_Ext.syn_ext' true is_logtype
-      mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
+    Syntax_Ext.syn_ext' is_logtype mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
   end;
 
 end;

--- a/src/Pure/Syntax/syntax.ML	Fri Apr 08 16:38:46 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Apr 08 17:45:37 2011 +0200
@@ -155,7 +155,7 @@
 
 (* configuration options *)
 
-val root = Config.string (Config.declare "syntax_root" (K (Config.String Syntax_Ext.any)));
+val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
 
 val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true);
 val positions = Config.bool positions_raw;
@@ -602,10 +602,10 @@
 val basic_syntax = update_syntax mode_default Syntax_Ext.pure_ext empty_syntax;
 
 val basic_nonterms =
-  (Lexicon.terminals @ [Syntax_Ext.logic, "type", "types", "sort", "classes",
-    Syntax_Ext.args, Syntax_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
-    "asms", Syntax_Ext.any, Syntax_Ext.sprop, "num_const", "float_const", "index",
-    "struct", "id_position", "longid_position", "type_name", "class_name"]);
+  (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
+    "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
+    "any", "prop'", "num_const", "float_const", "index", "struct",
+    "id_position", "longid_position", "type_name", "class_name"]);
 
 
 

--- a/src/Pure/Syntax/syntax_ext.ML	Fri Apr 08 16:38:46 2011 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Apr 08 17:45:37 2011 +0200
@@ -7,13 +7,6 @@
 signature SYNTAX_EXT =
 sig
   val dddot_indexname: indexname
-  val logic: string
-  val args: string
-  val cargs: string
-  val typeT: typ
-  val any: string
-  val sprop: string
-  val spropT: typ
   val max_pri: int
   datatype mfix = Mfix of string * typ * string * int list * int
   val err_in_mfix: string -> mfix -> 'a
@@ -39,7 +32,7 @@
   val mfix_delims: string -> string list
   val mfix_args: string -> int
   val escape: string -> string
-  val syn_ext': bool -> (string -> bool) -> mfix list ->
+  val syn_ext': (string -> bool) -> mfix list ->
     string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
@@ -79,24 +72,6 @@
 val dddot_indexname = ("dddot", 0);
 
 
-(* syntactic categories *)
-
-val logic = "logic";
-val logicT = Type (logic, []);
-
-val args = "args";
-val cargs = "cargs";
-
-val typeT = Type ("type", []);
-
-val sprop = "#prop";
-val spropT = Type (sprop, []);
-
-val any = "any";
-val anyT = Type (any, []);
-
-
-
 (** datatype xprod **)
 
 (*Delim s: delimiter s
@@ -165,10 +140,10 @@
   | typ_to_nt default _ = default;
 
 (*get nonterminal for rhs*)
-val typ_to_nonterm = typ_to_nt any;
+val typ_to_nonterm = typ_to_nt "any";
 
 (*get nonterminal for lhs*)
-val typ_to_nonterm1 = typ_to_nt logic;
+val typ_to_nonterm1 = typ_to_nt "logic";
 
 
 (* read mixfix annotations *)
@@ -219,7 +194,7 @@
 
 (* mfix_to_xprod *)
 
-fun mfix_to_xprod convert is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
+fun mfix_to_xprod is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
   let
     fun check_pri p =
       if p >= 0 andalso p <= max_pri then ()
@@ -255,7 +230,7 @@
       | rem_pri sym = sym;
 
     fun logify_types (a as (Argument (s, p))) =
-          if s <> "prop" andalso is_logtype s then Argument (logic, p) else a
+          if s <> "prop" andalso is_logtype s then Argument ("logic", p) else a
       | logify_types a = a;
 
 
@@ -287,8 +262,9 @@
         andalso not (null symbs)
         andalso not (exists is_delim symbs);
     val lhs' =
-      if convert andalso not copy_prod then
-       (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs)
+      if copy_prod orelse lhs = "prop" andalso symbs = [Argument ("prop'", 0)] then lhs
+      else if lhs = "prop" then "prop'"
+      else if is_logtype lhs then "logic"
       else lhs;
     val symbs' = map logify_types symbs;
     val xprod = XProd (lhs', symbs', const', pri);
@@ -322,12 +298,12 @@
 
 (* syn_ext *)
 
-fun syn_ext' convert is_logtype mfixes consts trfuns (parse_rules, print_rules) =
+fun syn_ext' is_logtype mfixes consts trfuns (parse_rules, print_rules) =
   let
     val (parse_ast_translation, parse_translation, print_translation,
       print_ast_translation) = trfuns;
 
-    val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
+    val (xprods, parse_rules') = map (mfix_to_xprod is_logtype) mfixes
       |> split_list |> apsnd (rev o flat);
     val mfix_consts =
       distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
@@ -344,7 +320,7 @@
   end;
 
 
-val syn_ext = syn_ext' true (K false);
+val syn_ext = syn_ext' (K false);
 
 fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) ([], []);
 fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules;
@@ -365,14 +341,16 @@
 val token_markers =
   ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"];
 
-val pure_ext = syn_ext' false (K false)
-  [Mfix ("_", spropT --> propT, "", [0], 0),
-   Mfix ("_", logicT --> anyT, "", [0], 0),
-   Mfix ("_", spropT --> anyT, "", [0], 0),
-   Mfix ("'(_')", logicT --> logicT, "", [0], max_pri),
-   Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
-   Mfix ("_::_",  [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3),
-   Mfix ("_::_",  [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
+val typ = Simple_Syntax.read_typ;
+
+val pure_ext = syn_ext' (K false)
+  [Mfix ("_", typ "prop' => prop", "", [0], 0),
+   Mfix ("_", typ "logic => any", "", [0], 0),
+   Mfix ("_", typ "prop' => any", "", [0], 0),
+   Mfix ("'(_')", typ "logic => logic", "", [0], max_pri),
+   Mfix ("'(_')", typ "prop' => prop'", "", [0], max_pri),
+   Mfix ("_::_", typ "logic => type => logic", "_constrain", [4, 0], 3),
+   Mfix ("_::_", typ "prop' => type => prop'", "_constrain", [4, 0], 3)]
   token_markers
   ([], [], [], [])
   ([], []);

--- a/src/Pure/pure_thy.ML	Fri Apr 08 16:38:46 2011 +0200
+++ b/src/Pure/pure_thy.ML	Fri Apr 08 17:45:37 2011 +0200
@@ -19,9 +19,6 @@
 val tycon = Lexicon.mark_type;
 val const = Lexicon.mark_const;
 
-val typeT = Syntax_Ext.typeT;
-val spropT = Syntax_Ext.spropT;
-
 
 (* application syntax variants *)
 
@@ -143,7 +140,7 @@
     ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
     ("_ofsort",           typ "tid => sort => type",    Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
     ("_constrain",        typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
-    ("_constrain",        [spropT, typeT] ---> spropT,  Mixfix ("_\\<Colon>_", [4, 0], 3)),
+    ("_constrain",        typ "prop' => type => prop'", Mixfix ("_\\<Colon>_", [4, 0], 3)),
     ("_idtyp",            typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
     ("_idtypdummy",       typ "type => idt",            Mixfix ("'_()\\<Colon>_", [], 0)),
     ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),