src/HOL/Tools/record.ML
changeset 35614 d7afa8700622
parent 35430 df2862dc23a8
child 35615 61bb9f8af129
     1.1 --- a/src/HOL/Tools/record.ML	Sat Mar 06 15:39:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Mar 06 16:13:22 2010 +0100
     1.3 @@ -896,25 +896,7 @@
     1.4  fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
     1.5    let
     1.6      val thy = ProofContext.theory_of ctxt;
     1.7 -
     1.8 -    (*tm is term representation of a (nested) field type. We first reconstruct the
     1.9 -      type from tm so that we can continue on the type level rather then the term level*)
    1.10 -
    1.11 -    (* FIXME !??? *)
    1.12 -    (*WORKAROUND:
    1.13 -      If a record type occurs in an error message of type inference there
    1.14 -      may be some internal frees donoted by ??:
    1.15 -      (Const "_tfree",_) $ Free ("??'a", _).
    1.16 -
    1.17 -      This will unfortunately be translated to Type ("??'a", []) instead of
    1.18 -      TFree ("??'a", _) by typ_of_term, which will confuse unify below.
    1.19 -      fixT works around.*)
    1.20 -    fun fixT (T as Type (x, [])) =
    1.21 -          if String.isPrefix "??'" x then TFree (x, Sign.defaultS thy) else T
    1.22 -      | fixT (Type (x, xs)) = Type (x, map fixT xs)
    1.23 -      | fixT T = T;
    1.24 -
    1.25 -    val T = fixT (decode_type thy tm);
    1.26 +    val T = decode_type thy tm;
    1.27      val midx = maxidx_of_typ T;
    1.28      val varifyT = varifyT midx;
    1.29