tuned;

--- a/src/HOL/Tools/record.ML	Sat Oct 17 20:37:38 2009 +0200
+++ b/src/HOL/Tools/record.ML	Sat Oct 17 21:14:08 2009 +0200
@@ -1597,9 +1597,9 @@
 fun extension_definition name fields alphas zeta moreT more vars thy =
   let
     val base = Long_Name.base_name;
-    val fieldTs = (map snd fields);
+    val fieldTs = map snd fields;
     val alphas_zeta = alphas @ [zeta];
-    val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
+    val alphas_zetaTs = map (fn a => TFree (a, HOLogic.typeS)) alphas_zeta;
     val extT_name = suffix ext_typeN name
     val extT = Type (extT_name, alphas_zetaTs);
     val fields_moreTs = fieldTs @ [moreT];