do not open ML structures;
authorwenzelm
Sun Mar 21 19:04:46 2010 +0100 (2010-03-21 ago)
changeset 358515c5f08f6d6e4
parent 35850 dd2636f0f608
child 35852 4e3fe0b8687b
do not open ML structures;
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