src/Pure/proofterm.ML
```     1.1 --- a/src/Pure/proofterm.ML	Sun Mar 21 17:28:35 2010 +0100
1.2 +++ b/src/Pure/proofterm.ML	Sun Mar 21 19:04:46 2010 +0100
1.3 @@ -812,24 +812,24 @@
1.4  val f = Free ("f", aT --> bT);
1.5  val g = Free ("g", aT --> bT);
1.6
1.7 -local open Logic in
1.8 -
1.9  val equality_axms =
1.10 -  [("reflexive", mk_equals (x, x)),
1.11 -   ("symmetric", mk_implies (mk_equals (x, y), mk_equals (y, x))),
1.12 -   ("transitive", list_implies ([mk_equals (x, y), mk_equals (y, z)], mk_equals (x, z))),
1.13 -   ("equal_intr", list_implies ([mk_implies (A, B), mk_implies (B, A)], mk_equals (A, B))),
1.14 -   ("equal_elim", list_implies ([mk_equals (A, B), A], B)),
1.15 -   ("abstract_rule", mk_implies
1.16 -      (all x (mk_equals (f \$ x, g \$ x)), mk_equals (lambda x (f \$ x), lambda x (g \$ x)))),
1.17 -   ("combination", list_implies
1.18 -      ([mk_equals (f, g), mk_equals (x, y)], mk_equals (f \$ x, g \$ y)))];
1.19 + [("reflexive", Logic.mk_equals (x, x)),
1.20 +  ("symmetric", Logic.mk_implies (Logic.mk_equals (x, y), Logic.mk_equals (y, x))),
1.21 +  ("transitive",
1.22 +    Logic.list_implies ([Logic.mk_equals (x, y), Logic.mk_equals (y, z)], Logic.mk_equals (x, z))),
1.23 +  ("equal_intr",
1.24 +    Logic.list_implies ([Logic.mk_implies (A, B), Logic.mk_implies (B, A)], Logic.mk_equals (A, B))),
1.25 +  ("equal_elim", Logic.list_implies ([Logic.mk_equals (A, B), A], B)),
1.26 +  ("abstract_rule",
1.27 +    Logic.mk_implies
1.28 +      (Logic.all x
1.29 +        (Logic.mk_equals (f \$ x, g \$ x)), Logic.mk_equals (lambda x (f \$ x), lambda x (g \$ x)))),
1.30 +  ("combination", Logic.list_implies
1.31 +    ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f \$ x, g \$ y)))];
1.32
1.33  val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm,
1.34    equal_elim_axm, abstract_rule_axm, combination_axm] =
1.35 -    map (fn (s, t) => PAxm ("Pure." ^ s, varify_global t, NONE)) equality_axms;
1.36 -
1.37 -end;
1.38 +    map (fn (s, t) => PAxm ("Pure." ^ s, Logic.varify_global t, NONE)) equality_axms;
1.39
1.40  val reflexive = reflexive_axm % NONE;
1.41
```