# HG changeset patch
# User schirmer
# Date 1148984644 -7200
# Node ID 5281bd607206276ecadf9ba78a45656e5b431a32
# Parent  a49881f91cce2e2d15fc4e32b319754c6d758a00
tuned type print-translations
----------------------------------------------------------------------

diff -r a49881f91cce -r 5281bd607206 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Mon May 29 21:09:45 2006 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue May 30 12:24:04 2006 +0200
@@ -583,7 +583,7 @@
 
                        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]))
@@ -739,7 +739,7 @@
                     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
@@ -775,7 +775,7 @@
                                 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)])