src/Pure/Syntax/syntax_phases.ML
changeset 52143 36ffe23b25f8
parent 50201 c26369c9eda6
child 52160 7746c9f1baf3
--- a/src/Pure/Syntax/syntax_phases.ML	Sat May 25 15:00:53 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat May 25 15:37:53 2013 +0200
@@ -751,10 +751,10 @@
 (* setup translations *)
 
 val _ = Context.>> (Context.map_theory
- (Sign.add_advanced_trfuns
-  ([("_context_const", const_ast_tr true),
-    ("_context_xconst", const_ast_tr false)], [], [], []) #>
-  Sign.add_advanced_trfunsT
+ (Sign.parse_ast_translation
+   [("_context_const", const_ast_tr true),
+    ("_context_xconst", const_ast_tr false)] #>
+  Sign.typed_print_translation
    [("_type_prop", type_prop_tr'),
     ("\\<^const>TYPE", type_tr'),
     ("_type_constraint_", type_constraint_tr')]));