src/Pure/logic.ML
changeset 32765 3032c0308019
parent 32026 9898880061df
child 32784 1a5dde5079ac
     1.1 --- a/src/Pure/logic.ML	Tue Sep 29 22:33:27 2009 +0200
     1.2 +++ b/src/Pure/logic.ML	Tue Sep 29 22:48:24 2009 +0200
     1.3 @@ -169,7 +169,7 @@
     1.4  
     1.5  (*(A &&& B) &&& (C &&& D) -- balanced*)
     1.6  fun mk_conjunction_balanced [] = true_prop
     1.7 -  | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
     1.8 +  | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
     1.9  
    1.10  
    1.11  (*A &&& B*)
    1.12 @@ -184,7 +184,7 @@
    1.13  
    1.14  (*(A &&& B) &&& (C &&& D) -- balanced*)
    1.15  fun dest_conjunction_balanced 0 _ = []
    1.16 -  | dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;
    1.17 +  | dest_conjunction_balanced n t = Balanced_Tree.dest dest_conjunction n t;
    1.18  
    1.19  (*((A &&& B) &&& C) &&& D &&& E -- flat*)
    1.20  fun dest_conjunctions t =