--- a/src/Pure/Isar/isar_syn.ML Fri Apr 08 22:40:29 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri Apr 08 22:50:50 2011 +0200
@@ -161,11 +161,11 @@
val _ =
Outer_Syntax.command "syntax" "declare syntactic constants" Keyword.thy_decl
- (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.add_modesyntax));
+ (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax));
val _ =
Outer_Syntax.command "no_syntax" "delete syntax declarations" Keyword.thy_decl
- (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.del_modesyntax));
+ (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax));
(* translations *)
--- a/src/Pure/Isar/parse.ML Fri Apr 08 22:40:29 2011 +0200
+++ b/src/Pure/Isar/parse.ML Fri Apr 08 22:50:50 2011 +0200
@@ -78,7 +78,7 @@
val opt_mixfix: mixfix parser
val opt_mixfix': mixfix parser
val where_: string parser
- val const: (string * string * mixfix) parser
+ val const_decl: (string * string * mixfix) parser
val const_binding: (binding * string * mixfix) parser
val params: (binding * string option) list parser
val simple_fixes: (binding * string option) list parser
@@ -295,7 +295,7 @@
val where_ = $$$ "where";
-val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
+val const_decl = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)