# HG changeset patch
# User wenzelm
# Date 901531773 -7200
# Node ID fac6fea3b7827e23d9a92c16ec18a0085150e3a6
# Parent  a23c23af335f7d2b505b8ee005634bb37a23ec5a
tuned;

diff -r a23c23af335f -r fac6fea3b782 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Mon Jul 27 09:18:24 1998 +0200
+++ b/src/HOL/Tools/record_package.ML	Mon Jul 27 11:29:33 1998 +0200
@@ -208,14 +208,14 @@
 
 fun gen_fields_tr sep mark sfx (tm as Const (c, _) $ t $ u) =
       if c = sep then gen_field_tr mark sfx t :: gen_fields_tr sep mark sfx u
-      else [gen_field_tr mark sfx  tm]
-  | gen_fields_tr _ mark sfx t = [gen_field_tr mark sfx t];
+      else [gen_field_tr mark sfx tm]
+  | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm];
 
 fun gen_record_tr sep mark sfx unit [t] = foldr (op $) (gen_fields_tr sep mark sfx t, unit)
-  | gen_record_tr _ _ _ _ ts = raise TERM ("record_tr", ts);
+  | gen_record_tr _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
 
 fun gen_record_scheme_tr sep mark sfx [t, more] = foldr (op $) (gen_fields_tr sep mark sfx t, more)
-  | gen_record_scheme_tr _ _ _ ts = raise TERM ("record_scheme_tr", ts);
+  | gen_record_scheme_tr _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
 
 
 val record_type_tr = gen_record_tr "_field_types" "_field_type" field_typeN (Syntax.const "unit");
@@ -239,10 +239,6 @@
 
 (* print translations *)
 
-fun gen_field_tr' sfx f name =
-  let val name_sfx = suffix sfx name
-  in (name_sfx, fn [t, u] => f (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
-
 fun gen_fields_tr' mark sfx (tm as Const (name_field, _) $ t $ u) =
       (case try (unsuffix sfx) name_field of
         Some name =>
@@ -274,6 +270,10 @@
   end;
 
 
+fun gen_field_tr' sfx tr' name =
+  let val name_sfx = suffix sfx name
+  in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
+
 fun print_translation names =
   map (gen_field_tr' field_typeN record_type_tr') names @
   map (gen_field_tr' fieldN record_tr') names @