src/Pure/sign.ML
changeset 52143 36ffe23b25f8
parent 47008 8b13ebf3eda4
child 56025 d74fed45fa8b
     1.1 --- a/src/Pure/sign.ML	Sat May 25 15:00:53 2013 +0200
     1.2 +++ b/src/Pure/sign.ML	Sat May 25 15:37:53 2013 +0200
     1.3 @@ -87,19 +87,16 @@
     1.4    val primitive_class: binding * class list -> theory -> theory
     1.5    val primitive_classrel: class * class -> theory -> theory
     1.6    val primitive_arity: arity -> theory -> theory
     1.7 -  val add_trfuns:
     1.8 -    (string * (Ast.ast list -> Ast.ast)) list *
     1.9 -    (string * (term list -> term)) list *
    1.10 -    (string * (term list -> term)) list *
    1.11 -    (string * (Ast.ast list -> Ast.ast)) list -> theory -> theory
    1.12 -  val add_trfunsT: (string * (typ -> term list -> term)) list -> theory -> theory
    1.13 -  val add_advanced_trfuns:
    1.14 -    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list *
    1.15 -    (string * (Proof.context -> term list -> term)) list *
    1.16 -    (string * (Proof.context -> term list -> term)) list *
    1.17 +  val parse_ast_translation:
    1.18      (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
    1.19 -  val add_advanced_trfunsT:
    1.20 +  val parse_translation:
    1.21 +    (string * (Proof.context -> term list -> term)) list -> theory -> theory
    1.22 +  val print_translation:
    1.23 +    (string * (Proof.context -> term list -> term)) list -> theory -> theory
    1.24 +  val typed_print_translation:
    1.25      (string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory
    1.26 +  val print_ast_translation:
    1.27 +    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
    1.28    val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
    1.29    val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
    1.30    val new_group: theory -> theory
    1.31 @@ -466,17 +463,14 @@
    1.32  
    1.33  fun mk trs = map Syntax_Ext.mk_trfun trs;
    1.34  
    1.35 -fun gen_add_trfuns ext non_typed (atrs, trs, tr's, atr's) =
    1.36 -  map_syn (ext (mk atrs, mk trs, mk (map (apsnd non_typed) tr's), mk atr's));
    1.37 -
    1.38 -fun gen_add_trfunsT ext tr's = map_syn (ext ([], [], mk tr's, []));
    1.39 -
    1.40  in
    1.41  
    1.42 -val add_trfuns = gen_add_trfuns Syntax.update_trfuns Syntax_Trans.non_typed_tr';
    1.43 -val add_trfunsT = gen_add_trfunsT Syntax.update_trfuns;
    1.44 -val add_advanced_trfuns = gen_add_trfuns Syntax.update_advanced_trfuns Syntax_Trans.non_typed_tr'';
    1.45 -val add_advanced_trfunsT = gen_add_trfunsT Syntax.update_advanced_trfuns;
    1.46 +fun parse_ast_translation atrs = map_syn (Syntax.update_trfuns (mk atrs, [], [], []));
    1.47 +fun parse_translation trs = map_syn (Syntax.update_trfuns ([], mk trs, [], []));
    1.48 +fun print_translation tr's =
    1.49 +  map_syn (Syntax.update_trfuns ([], [], mk (map (apsnd Syntax_Trans.non_typed_tr') tr's), []));
    1.50 +fun typed_print_translation tr's = map_syn (Syntax.update_trfuns ([], [], mk tr's, []));
    1.51 +fun print_ast_translation atr's = map_syn (Syntax.update_trfuns ([], [], [], mk atr's));
    1.52  
    1.53  end;
    1.54