src/HOL/Tools/Datatype/datatype_rep_proofs.ML
changeset 32765 3032c0308019
parent 32727 9072201cd69d
child 32874 5281cebb1a37
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -78,7 +78,7 @@
     val leafTs' = get_nonrec_types descr' sorts;
     val branchTs = get_branching_types descr' sorts;
     val branchT = if null branchTs then HOLogic.unitT
-      else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
+      else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
     val arities = get_arities descr' \ 0;
     val unneeded_vars = hd tyvars \\ List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs);
     val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
@@ -86,7 +86,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 BalancedTree.make (fn (T, U) => Type ("+", [T, U])) leafTs;
+      else Balanced_Tree.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;
@@ -116,7 +116,7 @@
 
     (* make injections for constructors *)
 
-    fun mk_univ_inj ts = BalancedTree.access
+    fun mk_univ_inj ts = Balanced_Tree.access
       {left = fn t => In0 $ t,
         right = fn t => In1 $ t,
         init =