# HG changeset patch
# User wenzelm
# Date 1302295850 -7200
# Node ID 06e93f257d0e99038413e85e0b440be420b7aa31
# Parent  d622145603eefe81048c042e5019eed105f4c02a
tuned signature;

diff -r d622145603ee -r 06e93f257d0e src/Pure/Isar/isar_syn.ML
--- 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 *)
diff -r d622145603ee -r 06e93f257d0e src/Pure/Isar/parse.ML
--- 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)