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)) =
```