src/ZF/Tools/datatype_package.ML
changeset 32765 3032c0308019
parent 30364 577edc39b501
child 32952 aeb1e44fbc19
     1.1 --- a/src/ZF/Tools/datatype_package.ML	Tue Sep 29 22:33:27 2009 +0200
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Tue Sep 29 22:48:24 2009 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4    fun mk_tuple [] = @{const "0"}
     1.5      | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
     1.6  
     1.7 -  fun mk_inject n k u = BalancedTree.access
     1.8 +  fun mk_inject n k u = Balanced_Tree.access
     1.9      {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = u} n k;
    1.10  
    1.11    val npart = length rec_names;  (*number of mutually recursive parts*)
    1.12 @@ -123,7 +123,7 @@
    1.13                  CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
    1.14                              @{typ i}
    1.15                              free
    1.16 -    in  BalancedTree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list)  end;
    1.17 +    in  Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list)  end;
    1.18  
    1.19    (** Generating function variables for the case definition
    1.20        Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
    1.21 @@ -158,7 +158,7 @@
    1.22    val case_tm = list_comb (case_const, case_args);
    1.23  
    1.24    val case_def = PrimitiveDefs.mk_defpair
    1.25 -    (case_tm, BalancedTree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
    1.26 +    (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
    1.27  
    1.28  
    1.29    (** Generating function variables for the recursor definition