src/HOL/Tools/Function/mutual.ML
changeset 32765 3032c0308019
parent 32149 ef59550a55d3
child 33099 b8cdd3d73022
--- a/src/HOL/Tools/Function/mutual.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -103,8 +103,8 @@
         val dresultTs = distinct (op =) resultTs
         val n' = length dresultTs
 
-        val RST = BalancedTree.make (uncurry SumTree.mk_sumT) dresultTs
-        val ST = BalancedTree.make (uncurry SumTree.mk_sumT) argTs
+        val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs
+        val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs
 
         val fsum_type = ST --> RST