src/HOL/Tools/record.ML

--- a/src/HOL/Tools/record.ML	Tue Feb 16 16:40:16 2010 +0100
+++ b/src/HOL/Tools/record.ML	Tue Feb 16 16:42:18 2010 +0100
@@ -929,7 +929,7 @@
 
 (*try to reconstruct the record name type abbreviation from
   the (nested) extension types*)
-fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt tm =
+fun record_type_abbr_tr' default_tr' abbr alphas zeta last_ext schemeT ctxt tm =
   let
     val thy = ProofContext.theory_of ctxt;
 
@@ -965,7 +965,7 @@
     if ! print_record_type_abbr then
       (case last_extT T of
         SOME (name, _) =>
-          if name = lastExt then
+          if name = last_ext then
            (let val subst = match schemeT T in
               if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, Sign.defaultS thy))))
               then mk_type_abbr subst abbr alphas
@@ -1035,7 +1035,7 @@
   in (name_sfx, tr') end;
 
 
-fun gen_record_type_abbr_tr' abbr alphas zeta lastExt schemeT name =
+fun gen_record_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
   let
     val name_sfx = suffix ext_typeN name;
     val default_tr' =
@@ -1045,7 +1045,7 @@
         @{syntax_const "_record_type"}
         @{syntax_const "_record_type_scheme"};
     fun tr' ctxt ts =
-      record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt
+      record_type_abbr_tr' default_tr' abbr alphas zeta last_ext schemeT ctxt
         (list_comb (Syntax.const name_sfx, ts));
   in (name_sfx, tr') end;
 
@@ -1981,8 +1981,8 @@
     val adv_record_type_abbr_tr's =
       let
         val trnames = external_names (hd extension_names);
-        val lastExt = unsuffix ext_typeN (fst extension);
-      in map (gen_record_type_abbr_tr' name alphas zeta lastExt rec_schemeT0) trnames end;
+        val last_ext = unsuffix ext_typeN (fst extension);
+      in map (gen_record_type_abbr_tr' name alphas zeta last_ext rec_schemeT0) trnames end;
 
     val adv_record_type_tr's =
       let