src/Pure/conjunction.ML
changeset 32765 3032c0308019
parent 30823 eb99b9134f2e
child 33277 1bdc3c732fdd
--- a/src/Pure/conjunction.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/Pure/conjunction.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -38,7 +38,7 @@
 fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
 
 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;
 
 fun dest_conjunction ct =
   (case Thm.term_of ct of
@@ -117,10 +117,10 @@
 (* balanced conjuncts *)
 
 fun intr_balanced [] = asm_rl
-  | intr_balanced ths = BalancedTree.make (uncurry intr) ths;
+  | intr_balanced ths = Balanced_Tree.make (uncurry intr) ths;
 
 fun elim_balanced 0 _ = []
-  | elim_balanced n th = BalancedTree.dest elim n th;
+  | elim_balanced n th = Balanced_Tree.dest elim n th;
 
 
 (* currying *)