eliminated camel case;
authorwenzelm
Tue Feb 16 16:42:18 2010 +0100 (2010-02-16)
changeset 351483a34fee2cfcd
parent 35147 9eb89f41c29d
child 35149 eee63670b5aa
eliminated camel case;
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Tools/record.ML	Tue Feb 16 16:40:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Tue Feb 16 16:42:18 2010 +0100
     1.3 @@ -929,7 +929,7 @@
     1.4  
     1.5  (*try to reconstruct the record name type abbreviation from
     1.6    the (nested) extension types*)
     1.7 -fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt tm =
     1.8 +fun record_type_abbr_tr' default_tr' abbr alphas zeta last_ext schemeT ctxt tm =
     1.9    let
    1.10      val thy = ProofContext.theory_of ctxt;
    1.11  
    1.12 @@ -965,7 +965,7 @@
    1.13      if ! print_record_type_abbr then
    1.14        (case last_extT T of
    1.15          SOME (name, _) =>
    1.16 -          if name = lastExt then
    1.17 +          if name = last_ext then
    1.18             (let val subst = match schemeT T in
    1.19                if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, Sign.defaultS thy))))
    1.20                then mk_type_abbr subst abbr alphas
    1.21 @@ -1035,7 +1035,7 @@
    1.22    in (name_sfx, tr') end;
    1.23  
    1.24  
    1.25 -fun gen_record_type_abbr_tr' abbr alphas zeta lastExt schemeT name =
    1.26 +fun gen_record_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
    1.27    let
    1.28      val name_sfx = suffix ext_typeN name;
    1.29      val default_tr' =
    1.30 @@ -1045,7 +1045,7 @@
    1.31          @{syntax_const "_record_type"}
    1.32          @{syntax_const "_record_type_scheme"};
    1.33      fun tr' ctxt ts =
    1.34 -      record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt
    1.35 +      record_type_abbr_tr' default_tr' abbr alphas zeta last_ext schemeT ctxt
    1.36          (list_comb (Syntax.const name_sfx, ts));
    1.37    in (name_sfx, tr') end;
    1.38  
    1.39 @@ -1981,8 +1981,8 @@
    1.40      val adv_record_type_abbr_tr's =
    1.41        let
    1.42          val trnames = external_names (hd extension_names);
    1.43 -        val lastExt = unsuffix ext_typeN (fst extension);
    1.44 -      in map (gen_record_type_abbr_tr' name alphas zeta lastExt rec_schemeT0) trnames end;
    1.45 +        val last_ext = unsuffix ext_typeN (fst extension);
    1.46 +      in map (gen_record_type_abbr_tr' name alphas zeta last_ext rec_schemeT0) trnames end;
    1.47  
    1.48      val adv_record_type_tr's =
    1.49        let