diff -r 098c86e53153 -r 578a51fae383 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Apr 05 14:25:18 2011 +0200
@@ -117,7 +117,7 @@
   ML_Lex.read pos txt
   |> ML_Context.expression pos
     ("val parse_ast_translation: (string * (" ^ advancedT a ^
-      "Syntax.ast list -> Syntax.ast)) list")
+      "Ast.ast list -> Ast.ast)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
   |> Context.theory_map;
 
@@ -141,7 +141,7 @@
   ML_Lex.read pos txt
   |> ML_Context.expression pos
     ("val print_ast_translation: (string * (" ^ advancedT a ^
-      "Syntax.ast list -> Syntax.ast)) list")
+      "Ast.ast list -> Ast.ast)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
   |> Context.theory_map;