src/HOL/Tools/record_package.ML

                                           Envir.norm_type subst o varifyT)
                                          (but_last alphas);
 
                        val more' = mk_ext rest;
                      in list_comb (Syntax.const (suffix sfx ext),alphas'@[more'])
-                     end handle TUNIFY => raise
+                     end handle TYPE_MATCH => raise
                            TERM (msg ^ "type is no proper record (extension)", [t]))
                | NONE => raise TERM (msg ^ "no fields defined for " ^ ext,[t]))
           | NONE => raise TERM (msg ^ name ^" is no proper field",[t]))
       | mk_ext [] = more
 

                      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
                     else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
-                   end handle TUNIFY => default_tr' context tm)
+                   end handle TYPE_MATCH => default_tr' context tm)
                  else raise Match (* give print translation of specialised record a chance *)
             | _ => raise Match)
        else default_tr' context tm
   end
 

                                 val subst= fold (Sign.typ_match thy) (alphavars~~args')
                                                     Vartab.empty;
                                 val flds'' =map (apsnd (Envir.norm_type subst o varifyT))
                                                 flds';
                               in flds''@field_lst more end
-                              handle TUNIFY         => [("",T)]
+                              handle TYPE_MATCH     => [("",T)]
                                    | UnequalLengths => [("",T)])
                          | NONE => [("",T)])
                    | NONE => [("",T)])
              | NONE => [("",T)])
         | _ => [("",T)])