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