src/Pure/sign.ML
changeset 22086 cf6019fece63
parent 21932 7d592dc078e3
child 22111 b3f5b654bcd3
     1.1 --- a/src/Pure/sign.ML	Fri Jan 19 13:09:32 2007 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Jan 19 13:09:33 2007 +0100
     1.3 @@ -840,31 +840,37 @@
     1.4  fun parse_ast_translation (a, txt) =
     1.5    txt |> Context.use_let ("val parse_ast_translation: (string * (" ^ advancedT a ^
     1.6        "Syntax.ast list -> Syntax.ast)) list")
     1.7 -    ("Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], [])");
     1.8 +    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
     1.9 +  |> Context.theory_map;
    1.10  
    1.11  fun parse_translation (a, txt) =
    1.12    txt |> Context.use_let ("val parse_translation: (string * (" ^ advancedT a ^
    1.13        "term list -> term)) list")
    1.14 -    ("Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], [])");
    1.15 +    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
    1.16 +  |> Context.theory_map;
    1.17  
    1.18  fun print_translation (a, txt) =
    1.19    txt |> Context.use_let ("val print_translation: (string * (" ^ advancedT a ^
    1.20        "term list -> term)) list")
    1.21 -    ("Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, [])");
    1.22 +    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
    1.23 +  |> Context.theory_map;
    1.24  
    1.25  fun print_ast_translation (a, txt) =
    1.26    txt |> Context.use_let ("val print_ast_translation: (string * (" ^ advancedT a ^
    1.27        "Syntax.ast list -> Syntax.ast)) list")
    1.28 -    ("Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation)");
    1.29 +    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
    1.30 +  |> Context.theory_map;
    1.31  
    1.32  fun typed_print_translation (a, txt) =
    1.33    txt |> Context.use_let ("val typed_print_translation: (string * (" ^ advancedT a ^
    1.34        "bool -> typ -> term list -> term)) list")
    1.35 -    ("Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation");
    1.36 +    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
    1.37 +  |> Context.theory_map;
    1.38  
    1.39  val token_translation =
    1.40    Context.use_let "val token_translation: (string * string * (string -> string * real)) list"
    1.41 -    "Sign.add_tokentrfuns token_translation";
    1.42 +    "Context.map_theory (Sign.add_tokentrfuns token_translation)"
    1.43 +  #> Context.theory_map;
    1.44  
    1.45  end;
    1.46