src/HOL/Tools/Nitpick/nitpick_mono.ML

                 x = x' andalso ((sn = sn' andalso a <> a') orelse
                                 (sn <> sn' andalso a = a'))
               | _ => 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)
 
 fun add_assign_clause NONE = I

        SOME cset)
     |> do_mtype_comp Leq xs M12 M22
   | 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 *)
   | do_mtype_comp cmp _ M1 M2 _ =
     raise MTYPE ("Nitpick_Mono.do_mtype_comp (" ^ string_for_comp_op cmp ^ ")",