1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 06 13:33:09 2010 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 06 13:36:28 2010 +0100
1.3 @@ -387,7 +387,7 @@
1.4 | _ => false) clauses then
1.5 NONE
1.6 else
1.7 - SOME ([(x, a)] :: clauses)
1.8 + SOME ([(x, (sn, a))] :: clauses)
1.9
1.10 fun add_assign_disjunct _ NONE = NONE
1.11 | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs)
1.12 @@ -445,7 +445,7 @@
1.13 | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22))
1.14 cset =
1.15 (cset |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
1.16 - handle Library.UnequalLengths =>
1.17 + handle ListPair.UnequalLengths =>
1.18 raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], []))
1.19 | do_mtype_comp _ _ (MType _) (MType _) cset =
1.20 cset (* no need to compare them thanks to the cache *)