1.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Apr 03 18:17:21 2011 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Apr 03 21:59:33 2011 +0200
     1.3 @@ -175,9 +175,9 @@
     1.4      -- Parse.string;
     1.5  
     1.6  fun trans_arrow toks =
     1.7 -  ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.ParseRule ||
     1.8 -    (Parse.$$$ "\\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.PrintRule ||
     1.9 -    (Parse.$$$ "\\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.ParsePrintRule) toks;
    1.10 +  ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.Parse_Rule ||
    1.11 +    (Parse.$$$ "\\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.Print_Rule ||
    1.12 +    (Parse.$$$ "\\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.Parse_Print_Rule) toks;
    1.13  
    1.14  val trans_line =
    1.15    trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
    1.16 @@ -185,11 +185,11 @@
    1.17  
    1.18  val _ =
    1.19    Outer_Syntax.command "translations" "declare syntax translation rules" Keyword.thy_decl
    1.20 -    (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules));
    1.21 +    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
    1.22  
    1.23  val _ =
    1.24    Outer_Syntax.command "no_translations" "remove syntax translation rules" Keyword.thy_decl
    1.25 -    (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules));
    1.26 +    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
    1.27  
    1.28  
    1.29  (* axioms and definitions *)