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