src/Pure/Isar/isar_cmd.ML
changeset 42224 578a51fae383
parent 42204 b3277168c1e7
child 42242 39261908e12f
--- 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;