compile
authorblanchet
Mon Dec 06 13:36:28 2010 +0100 (2010-12-06)
changeset 41017666d8ed0b73a
parent 41016 343cdf923c02
child 41018 83f241623b86
compile
src/HOL/Tools/Nitpick/nitpick_mono.ML
     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 *)