--- a/src/Pure/pure_thy.ML Wed Mar 03 00:00:44 2010 +0100
+++ b/src/Pure/pure_thy.ML Wed Mar 03 00:28:22 2010 +0100
@@ -225,6 +225,8 @@
val typ = Simple_Syntax.read_typ;
val prop = Simple_Syntax.read_prop;
+
+val tycon = Syntax.mark_type;
val const = Syntax.mark_const;
val typeT = Syntax.typeT;
@@ -318,21 +320,21 @@
(const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
#> Sign.add_syntax_i applC_syntax
#> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
- [("fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
- ("_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)),
- ("_idtyp", typ "id => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
- ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
- ("_type_constraint_", typ "'a", NoSyn),
- ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
- (const "==", typ "'a => 'a => prop", Infixr ("\\<equiv>", 2)),
- (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
- (const "==>", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
- ("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
- ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
- ("_DDDOT", typ "logic", Delimfix "\\<dots>")]
+ [(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
+ ("_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)),
+ ("_idtyp", typ "id => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
+ ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
+ ("_type_constraint_", typ "'a", NoSyn),
+ ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
+ (const "==", typ "'a => 'a => prop", Infixr ("\\<equiv>", 2)),
+ (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
+ (const "==>", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
+ ("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
+ ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
+ ("_DDDOT", typ "logic", Delimfix "\\<dots>")]
#> Sign.add_modesyntax_i ("", false)
[(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
#> Sign.add_modesyntax_i ("HTML", false)