--- a/src/elaborate.sml	Wed Nov 25 09:30:44 2009 -0500
+++ b/src/elaborate.sml	Wed Nov 25 09:48:23 2009 -0500
@@ -4017,11 +4017,33 @@
                           | (_, true) => (oneSummaryRound (); solver gs)
                           | _ =>
                             app (fn Disjoint (loc, env, denv, c1, c2) =>
-                                    ((ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
-                                      eprefaces' [("Con 1", p_con env c1),
-                                                  ("Con 2", p_con env c2),
-                                                  ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
-                                                  ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))]))
+                                    let
+                                        val c1' = ElabOps.hnormCon env c1
+                                        val c2' = ElabOps.hnormCon env c2
+
+                                        fun isUnif (c, _) =
+                                            case c of
+                                                L'.CUnif _ => true
+                                              | _ => false
+
+                                        fun maybeAttr (c, _) =
+                                            case c of
+                                                L'.CRecord ((L'.KType, _), xts) => true
+                                              | _ => false
+                                    in
+                                        ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
+                                        eprefaces' [("Con 1", p_con env c1),
+                                                    ("Con 2", p_con env c2),
+                                                    ("Hnormed 1", p_con env c1'),
+                                                    ("Hnormed 2", p_con env c2')];
+
+                                        if (isUnif c1' andalso maybeAttr c2')
+                                           orelse (isUnif c2' andalso maybeAttr c1') then
+                                            TextIO.output (TextIO.stdErr,
+                                                           "You may be using a disallowed attribute with an HTML tag.\n")
+                                        else
+                                            ()
+                                    end
                                   | TypeClass (env, c, r, loc) =>
                                     expError env (Unresolvable (loc, c)))
                                 gs