src/Pure/axclass.ML
changeset 32765 3032c0308019
parent 32197 bc341bbe4417
child 32791 e6d47ce70d27
     1.1 --- a/src/Pure/axclass.ML	Tue Sep 29 22:33:27 2009 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Sep 29 22:48:24 2009 +0200
     1.3 @@ -419,7 +419,7 @@
     1.4        if n = 0 then []
     1.5        else
     1.6          (eq RS Drule.equal_elim_rule1)
     1.7 -        |> BalancedTree.dest (fn th =>
     1.8 +        |> Balanced_Tree.dest (fn th =>
     1.9            (th RS Conjunction.conjunctionD1, th RS Conjunction.conjunctionD2)) n;
    1.10    in (intro, dests) end;
    1.11