src/HOL/Tools/record_package.ML
changeset 5201 fac6fea3b782
parent 5197 69c77ed95ba3
child 5210 54aaa779b6b4
     1.1 --- a/src/HOL/Tools/record_package.ML	Mon Jul 27 09:18:24 1998 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Mon Jul 27 11:29:33 1998 +0200
     1.3 @@ -208,14 +208,14 @@
     1.4  
     1.5  fun gen_fields_tr sep mark sfx (tm as Const (c, _) $ t $ u) =
     1.6        if c = sep then gen_field_tr mark sfx t :: gen_fields_tr sep mark sfx u
     1.7 -      else [gen_field_tr mark sfx  tm]
     1.8 -  | gen_fields_tr _ mark sfx t = [gen_field_tr mark sfx t];
     1.9 +      else [gen_field_tr mark sfx tm]
    1.10 +  | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm];
    1.11  
    1.12  fun gen_record_tr sep mark sfx unit [t] = foldr (op $) (gen_fields_tr sep mark sfx t, unit)
    1.13 -  | gen_record_tr _ _ _ _ ts = raise TERM ("record_tr", ts);
    1.14 +  | gen_record_tr _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
    1.15  
    1.16  fun gen_record_scheme_tr sep mark sfx [t, more] = foldr (op $) (gen_fields_tr sep mark sfx t, more)
    1.17 -  | gen_record_scheme_tr _ _ _ ts = raise TERM ("record_scheme_tr", ts);
    1.18 +  | gen_record_scheme_tr _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
    1.19  
    1.20  
    1.21  val record_type_tr = gen_record_tr "_field_types" "_field_type" field_typeN (Syntax.const "unit");
    1.22 @@ -239,10 +239,6 @@
    1.23  
    1.24  (* print translations *)
    1.25  
    1.26 -fun gen_field_tr' sfx f name =
    1.27 -  let val name_sfx = suffix sfx name
    1.28 -  in (name_sfx, fn [t, u] => f (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
    1.29 -
    1.30  fun gen_fields_tr' mark sfx (tm as Const (name_field, _) $ t $ u) =
    1.31        (case try (unsuffix sfx) name_field of
    1.32          Some name =>
    1.33 @@ -274,6 +270,10 @@
    1.34    end;
    1.35  
    1.36  
    1.37 +fun gen_field_tr' sfx tr' name =
    1.38 +  let val name_sfx = suffix sfx name
    1.39 +  in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
    1.40 +
    1.41  fun print_translation names =
    1.42    map (gen_field_tr' field_typeN record_type_tr') names @
    1.43    map (gen_field_tr' fieldN record_tr') names @