# HG changeset patch
# User schirmer
# Date 1171899848 -3600
# Node ID 0dc6b45e5662d584770bb467b8849cffa49a5d23
# Parent  c7feeba2249e621b3cdce0ff774016bf8b700e9f
more precise error message in parameter unification

diff -r c7feeba2249e -r 0dc6b45e5662 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Feb 17 18:01:22 2007 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Feb 19 16:44:08 2007 +0100
@@ -603,9 +603,13 @@
 
     fun unify T U envir = Sign.typ_unify thy (U, T) envir
       handle Type.TUNIFY =>
-        let val prt = Sign.string_of_typ thy in
+        let 
+          val T' = Envir.norm_type (fst envir) T;
+          val U' = Envir.norm_type (fst envir) U;
+          val prt = Sign.string_of_typ thy; 
+        in
           raise TYPE ("unify_parms: failed to unify types " ^
-            prt U ^ " and " ^ prt T, [U, T], [])
+            prt U' ^ " and " ^ prt T', [U', T'], [])
         end;
     fun unify_list (T :: Us) = fold (unify T) Us
       | unify_list [] = I;