src/Pure/Syntax/syntax.ML
changeset 4618 731bed12f762
parent 4496 16187138463d
child 4703 a50ab39756db
     1.1 --- a/src/Pure/Syntax/syntax.ML	Thu Feb 12 12:36:28 1998 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Feb 12 12:36:55 1998 +0100
     1.3 @@ -40,6 +40,7 @@
     1.4    val extend_tokentrfuns: syntax -> (string * string * (string -> string * int)) list -> syntax
     1.5    val extend_trrules: syntax -> (string * string) trrule list -> syntax
     1.6    val extend_trrules_i: syntax -> ast trrule list -> syntax
     1.7 +  val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
     1.8    val merge_syntaxes: syntax -> syntax -> syntax
     1.9    val type_syn: syntax
    1.10    val pure_syn: syntax
    1.11 @@ -397,9 +398,9 @@
    1.12    PrintRule of 'a * 'a |
    1.13    ParsePrintRule of 'a * 'a;
    1.14  
    1.15 -fun map_rule f (ParseRule (x, y)) = ParseRule (f x, f y)
    1.16 -  | map_rule f (PrintRule (x, y)) = PrintRule (f x, f y)
    1.17 -  | map_rule f (ParsePrintRule (x, y)) = ParsePrintRule (f x, f y);
    1.18 +fun map_trrule f (ParseRule (x, y)) = ParseRule (f x, f y)
    1.19 +  | map_trrule f (PrintRule (x, y)) = PrintRule (f x, f y)
    1.20 +  | map_trrule f (ParsePrintRule (x, y)) = ParsePrintRule (f x, f y);
    1.21  
    1.22  fun parse_rule (ParseRule pats) = Some pats
    1.23    | parse_rule (PrintRule _) = None
    1.24 @@ -437,7 +438,7 @@
    1.25  
    1.26  
    1.27  fun prep_rules rd_pat raw_rules =
    1.28 -  let val rules = map (map_rule rd_pat) raw_rules in
    1.29 +  let val rules = map (map_trrule rd_pat) raw_rules in
    1.30      (map check_rule (mapfilter parse_rule rules),
    1.31        map check_rule (mapfilter print_rule rules))
    1.32    end