tuned signature;
authorwenzelm
Fri Apr 08 22:50:50 2011 +0200 (2011-04-08 ago)
changeset 4229906e93f257d0e
parent 42298 d622145603ee
child 42300 0d1cbc1fe579
tuned signature;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/parse.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Apr 08 22:40:29 2011 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 08 22:50:50 2011 +0200
     1.3 @@ -161,11 +161,11 @@
     1.4  
     1.5  val _ =
     1.6    Outer_Syntax.command "syntax" "declare syntactic constants" Keyword.thy_decl
     1.7 -    (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.add_modesyntax));
     1.8 +    (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax));
     1.9  
    1.10  val _ =
    1.11    Outer_Syntax.command "no_syntax" "delete syntax declarations" Keyword.thy_decl
    1.12 -    (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.del_modesyntax));
    1.13 +    (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax));
    1.14  
    1.15  
    1.16  (* translations *)
     2.1 --- a/src/Pure/Isar/parse.ML	Fri Apr 08 22:40:29 2011 +0200
     2.2 +++ b/src/Pure/Isar/parse.ML	Fri Apr 08 22:50:50 2011 +0200
     2.3 @@ -78,7 +78,7 @@
     2.4    val opt_mixfix: mixfix parser
     2.5    val opt_mixfix': mixfix parser
     2.6    val where_: string parser
     2.7 -  val const: (string * string * mixfix) parser
     2.8 +  val const_decl: (string * string * mixfix) parser
     2.9    val const_binding: (binding * string * mixfix) parser
    2.10    val params: (binding * string option) list parser
    2.11    val simple_fixes: (binding * string option) list parser
    2.12 @@ -295,7 +295,7 @@
    2.13  
    2.14  val where_ = $$$ "where";
    2.15  
    2.16 -val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
    2.17 +val const_decl = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
    2.18  val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
    2.19  
    2.20  val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)