tuned type print-translations
----------------------------------------------------------------------
--- 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)])