src/HOL/Tools/Function/sum_tree.ML
changeset 32765 3032c0308019
parent 32603 e08fdd615333
child 33961 03f2ab6a4ea6
--- a/src/HOL/Tools/Function/sum_tree.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/HOL/Tools/Function/sum_tree.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -13,7 +13,7 @@
 
 (* top-down access in balanced tree *)
 fun access_top_down {left, right, init} len i =
-    BalancedTree.access {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
+    Balanced_Tree.access {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
 
 (* Sum types *)
 fun mk_sumT LT RT = Type ("+", [LT, RT])
@@ -36,7 +36,7 @@
     |> snd
 
 fun mk_sumcases T fs =
-      BalancedTree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) 
+      Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) 
                         (map (fn f => (f, domain_type (fastype_of f))) fs)
       |> fst