src/HOL/Tools/Nitpick/nitpick_peephole.ML
changeset 34126 8a2c5d7aff51
parent 34124 c4628a1dcf75
child 34936 c4f04bee79f3
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Thu Dec 17 15:22:27 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Fri Dec 18 12:00:29 2009 +0100
     1.3 @@ -266,7 +266,7 @@
     1.4  
     1.5      (* bool -> int *)
     1.6      val from_bool = atom_for_bool main_j0
     1.7 -    (* int -> Kodkod.rel_expr *)
     1.8 +    (* int -> rel_expr *)
     1.9      fun from_nat n = Atom (n + main_j0)
    1.10      val from_int = Atom o atom_for_int (int_card, main_j0)
    1.11      (* int -> int *)
    1.12 @@ -347,7 +347,7 @@
    1.13      (* rel_expr -> formula *)
    1.14      fun s_no None = True
    1.15        | s_no (Product (r1, r2)) = s_or (s_no r1) (s_no r2)
    1.16 -      | s_no (Intersect (Closure (Kodkod.Rel x), Kodkod.Iden)) = Acyclic x
    1.17 +      | s_no (Intersect (Closure (Rel x), Iden)) = Acyclic x
    1.18        | s_no r = if is_one_rel_expr r then False else No r
    1.19      fun s_lone None = True
    1.20        | s_lone r = if is_one_rel_expr r then True else Lone r
    1.21 @@ -409,8 +409,8 @@
    1.22                      s_formula_if f (s_rel_eq r11 r2) (s_rel_eq r12 r2)
    1.23                    else
    1.24                      RelEq (r1, r2)
    1.25 -               | (_, Kodkod.None) => s_no r1
    1.26 -               | (Kodkod.None, _) => s_no r2
    1.27 +               | (_, None) => s_no r1
    1.28 +               | (None, _) => s_no r2
    1.29                 | _ => RelEq (r1, r2)
    1.30      fun s_subset (Atom j1) (Atom j2) = formula_for_bool (j1 = j2)
    1.31        | s_subset (Atom j) (AtomSeq (k, j0)) =