# HG changeset patch
# User blanchet
# Date 1291638988 -3600
# Node ID 666d8ed0b73a627894f41cf1dff1bfb59b6f6cd3
# Parent  343cdf923c023a8fb2b650def35059a3e94186bc
compile

diff -r 343cdf923c02 -r 666d8ed0b73a src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:36:28 2010 +0100
@@ -387,7 +387,7 @@
               | _ => false) clauses then
     NONE
   else
-    SOME ([(x, a)] :: clauses)
+    SOME ([(x, (sn, a))] :: clauses)
 
 fun add_assign_disjunct _ NONE = NONE
   | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs)
@@ -445,7 +445,7 @@
   | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22))
                   cset =
     (cset |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
-     handle Library.UnequalLengths =>
+     handle ListPair.UnequalLengths =>
             raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], []))
   | do_mtype_comp _ _ (MType _) (MType _) cset =
     cset (* no need to compare them thanks to the cache *)