--- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Jun 19 23:15:27 2007 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Jun 19 23:15:38 2007 +0200
@@ -77,7 +77,7 @@
val leafTs' = get_nonrec_types descr' sorts;
val branchTs = get_branching_types descr' sorts;
val branchT = if null branchTs then HOLogic.unitT
- else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
+ else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
val arities = get_arities descr' \ 0;
val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names [] (leafTs' @ branchTs);
val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
@@ -85,7 +85,7 @@
val newTs = Library.take (length (hd descr), recTs);
val oldTs = Library.drop (length (hd descr), recTs);
val sumT = if null leafTs then HOLogic.unitT
- else fold_bal (fn (T, U) => Type ("+", [T, U])) leafTs;
+ else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) leafTs;
val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
val UnivT = HOLogic.mk_setT Univ_elT;
val UnivT' = Univ_elT --> HOLogic.boolT;
@@ -115,10 +115,12 @@
(* make injections for constructors *)
- fun mk_univ_inj ts = access_bal (fn t => In0 $ t, fn t => In1 $ t, if ts = [] then
- Const ("arbitrary", Univ_elT)
- else
- foldr1 (HOLogic.mk_binop Scons_name) ts);
+ fun mk_univ_inj ts = BalancedTree.access
+ {left = fn t => In0 $ t,
+ right = fn t => In1 $ t,
+ init =
+ if ts = [] then Const ("arbitrary", Univ_elT)
+ else foldr1 (HOLogic.mk_binop Scons_name) ts};
(* function spaces *)