src/Pure/pure_thy.ML
changeset 52143 36ffe23b25f8
parent 51612 6a1e40f9dd55
child 52160 7746c9f1baf3
     1.1 --- a/src/Pure/pure_thy.ML	Sat May 25 15:00:53 2013 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Sat May 25 15:37:53 2013 +0200
     1.3 @@ -189,7 +189,9 @@
     1.4    #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
     1.5    #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
     1.6    #> Theory.add_deps_global Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
     1.7 -  #> Sign.add_trfuns Syntax_Trans.pure_trfuns
     1.8 +  #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
     1.9 +  #> Sign.parse_translation Syntax_Trans.pure_parse_translation
    1.10 +  #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
    1.11    #> Sign.local_path
    1.12    #> Sign.add_consts_i
    1.13     [(Binding.name "term", typ "'a => prop", NoSyn),