src/Pure/logic.ML
changeset 32765 3032c0308019
parent 32026 9898880061df
child 32784 1a5dde5079ac
--- a/src/Pure/logic.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/Pure/logic.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -169,7 +169,7 @@
 
 (*(A &&& B) &&& (C &&& D) -- balanced*)
 fun mk_conjunction_balanced [] = true_prop
-  | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
+  | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
 
 
 (*A &&& B*)
@@ -184,7 +184,7 @@
 
 (*(A &&& B) &&& (C &&& D) -- balanced*)
 fun dest_conjunction_balanced 0 _ = []
-  | dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;
+  | dest_conjunction_balanced n t = Balanced_Tree.dest dest_conjunction n t;
 
 (*((A &&& B) &&& C) &&& D &&& E -- flat*)
 fun dest_conjunctions t =