tuned;
authorwenzelm
Sat Oct 17 21:14:08 2009 +0200 (2009-10-17)
changeset 32977d83b9ad78d4b
parent 32976 38364667c773
child 32978 a473ba9a221d
tuned;
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Tools/record.ML	Sat Oct 17 20:37:38 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Oct 17 21:14:08 2009 +0200
     1.3 @@ -1597,9 +1597,9 @@
     1.4  fun extension_definition name fields alphas zeta moreT more vars thy =
     1.5    let
     1.6      val base = Long_Name.base_name;
     1.7 -    val fieldTs = (map snd fields);
     1.8 +    val fieldTs = map snd fields;
     1.9      val alphas_zeta = alphas @ [zeta];
    1.10 -    val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
    1.11 +    val alphas_zetaTs = map (fn a => TFree (a, HOLogic.typeS)) alphas_zeta;
    1.12      val extT_name = suffix ext_typeN name
    1.13      val extT = Type (extT_name, alphas_zetaTs);
    1.14      val fields_moreTs = fieldTs @ [moreT];