# HG changeset patch
# User wenzelm
# Date 1254257304 -7200
# Node ID 3032c03080198608e66666642a286c9dca28e441
# Parent  690f9cccf232ed975e33a75b933c624c58b70df1
modernized Balanced_Tree;

diff -r 690f9cccf232 -r 3032c0308019 src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- 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 =
diff -r 690f9cccf232 -r 3032c0308019 src/HOL/Tools/Function/induction_scheme.ML
--- a/src/HOL/Tools/Function/induction_scheme.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/HOL/Tools/Function/induction_scheme.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -120,7 +120,7 @@
       fun PT_of (SchemeBranch { xs, ...}) =
             foldr1 HOLogic.mk_prodT (map snd xs)
 
-      val ST = BalancedTree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
+      val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
     in
       IndScheme {T=ST, cases=map mk_case cases', branches=branches }
     end
diff -r 690f9cccf232 -r 3032c0308019 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -103,8 +103,8 @@
         val dresultTs = distinct (op =) resultTs
         val n' = length dresultTs
 
-        val RST = BalancedTree.make (uncurry SumTree.mk_sumT) dresultTs
-        val ST = BalancedTree.make (uncurry SumTree.mk_sumT) argTs
+        val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs
+        val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs
 
         val fsum_type = ST --> RST
 
diff -r 690f9cccf232 -r 3032c0308019 src/HOL/Tools/Function/sum_tree.ML
--- 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
 
diff -r 690f9cccf232 -r 3032c0308019 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/HOL/Tools/record.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -1732,7 +1732,7 @@
 
     (*before doing anything else, create the tree of new types
       that will back the record extension*)
-    (* FIXME cf. BalancedTree.make *)
+    (* FIXME cf. Balanced_Tree.make *)
     fun mktreeT [] = raise TYPE ("mktreeT: empty list", [], [])
       | mktreeT [T] = T
       | mktreeT xs =
@@ -1745,7 +1745,7 @@
             HOLogic.mk_prodT (mktreeT left, mktreeT right)
           end;
 
-    (* FIXME cf. BalancedTree.make *)
+    (* FIXME cf. Balanced_Tree.make *)
     fun mktreeV [] = raise TYPE ("mktreeV: empty list", [], [])
       | mktreeV [T] = T
       | mktreeV xs =
diff -r 690f9cccf232 -r 3032c0308019 src/Pure/General/balanced_tree.ML
--- a/src/Pure/General/balanced_tree.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/Pure/General/balanced_tree.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -12,7 +12,7 @@
   val accesses: {left: 'a -> 'a, right: 'a -> 'a, init: 'a} -> int -> 'a list
 end;
 
-structure BalancedTree: BALANCED_TREE =
+structure Balanced_Tree: BALANCED_TREE =
 struct
 
 fun make _ [] = raise Empty
diff -r 690f9cccf232 -r 3032c0308019 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/Pure/axclass.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -419,7 +419,7 @@
       if n = 0 then []
       else
         (eq RS Drule.equal_elim_rule1)
-        |> BalancedTree.dest (fn th =>
+        |> Balanced_Tree.dest (fn th =>
           (th RS Conjunction.conjunctionD1, th RS Conjunction.conjunctionD2)) n;
   in (intro, dests) end;
 
diff -r 690f9cccf232 -r 3032c0308019 src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/Pure/conjunction.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -38,7 +38,7 @@
 fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
 
 fun mk_conjunction_balanced [] = true_prop
-  | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
+  | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
 
 fun dest_conjunction ct =
   (case Thm.term_of ct of
@@ -117,10 +117,10 @@
 (* balanced conjuncts *)
 
 fun intr_balanced [] = asm_rl
-  | intr_balanced ths = BalancedTree.make (uncurry intr) ths;
+  | intr_balanced ths = Balanced_Tree.make (uncurry intr) ths;
 
 fun elim_balanced 0 _ = []
-  | elim_balanced n th = BalancedTree.dest elim n th;
+  | elim_balanced n th = Balanced_Tree.dest elim n th;
 
 
 (* currying *)
diff -r 690f9cccf232 -r 3032c0308019 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/Pure/logic.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -169,7 +169,7 @@
 
 (*(A &&& B) &&& (C &&& D) -- balanced*)
 fun mk_conjunction_balanced [] = true_prop
-  | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
+  | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
 
 
 (*A &&& B*)
@@ -184,7 +184,7 @@
 
 (*(A &&& B) &&& (C &&& D) -- balanced*)
 fun dest_conjunction_balanced 0 _ = []
-  | dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;
+  | dest_conjunction_balanced n t = Balanced_Tree.dest dest_conjunction n t;
 
 (*((A &&& B) &&& C) &&& D &&& E -- flat*)
 fun dest_conjunctions t =
diff -r 690f9cccf232 -r 3032c0308019 src/ZF/Datatype_ZF.thy
--- a/src/ZF/Datatype_ZF.thy	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/ZF/Datatype_ZF.thy	Tue Sep 29 22:48:24 2009 +0200
@@ -63,7 +63,7 @@
 
   fun mk_new ([],[]) = Const("True",FOLogic.oT)
     | mk_new (largs,rargs) =
-        BalancedTree.make FOLogic.mk_conj
+        Balanced_Tree.make FOLogic.mk_conj
                  (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
 
  val datatype_ss = @{simpset};
diff -r 690f9cccf232 -r 3032c0308019 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -94,7 +94,7 @@
   fun mk_tuple [] = @{const "0"}
     | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
 
-  fun mk_inject n k u = BalancedTree.access
+  fun mk_inject n k u = Balanced_Tree.access
     {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = u} n k;
 
   val npart = length rec_names;  (*number of mutually recursive parts*)
@@ -123,7 +123,7 @@
                 CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
                             @{typ i}
                             free
-    in  BalancedTree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list)  end;
+    in  Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list)  end;
 
   (** Generating function variables for the case definition
       Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
@@ -158,7 +158,7 @@
   val case_tm = list_comb (case_const, case_args);
 
   val case_def = PrimitiveDefs.mk_defpair
-    (case_tm, BalancedTree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
+    (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
 
 
   (** Generating function variables for the recursor definition
diff -r 690f9cccf232 -r 3032c0308019 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -113,7 +113,7 @@
         val exfrees = OldTerm.term_frees intr \\ rec_params
         val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
     in List.foldr FOLogic.mk_exists
-             (BalancedTree.make FOLogic.mk_conj (zeq::prems)) exfrees
+             (Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees
     end;
 
   (*The Part(A,h) terms -- compose injections to make h*)
@@ -122,7 +122,7 @@
 
   (*Access to balanced disjoint sums via injections*)
   val parts = map mk_Part
-    (BalancedTree.accesses {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = Bound 0}
+    (Balanced_Tree.accesses {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = Bound 0}
       (length rec_tms));
 
   (*replace each set by the corresponding Part(A,h)*)
@@ -130,7 +130,7 @@
 
   val fp_abs = absfree(X', iT,
                    mk_Collect(z', dom_sum,
-                              BalancedTree.make FOLogic.mk_disj part_intrs));
+                              Balanced_Tree.make FOLogic.mk_disj part_intrs));
 
   val fp_rhs = Fp.oper $ dom_sum $ fp_abs
 
@@ -238,7 +238,7 @@
      DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
 
   (*combines disjI1 and disjI2 to get the corresponding nested disjunct...*)
-  val mk_disj_rls = BalancedTree.accesses
+  val mk_disj_rls = Balanced_Tree.accesses
     {left = fn rl => rl RS @{thm disjI1},
      right = fn rl => rl RS @{thm disjI2},
      init = @{thm asm_rl}};
@@ -398,10 +398,10 @@
            (Ind_Syntax.mk_all_imp
             (big_rec_tm,
              Abs("z", Ind_Syntax.iT,
-                 BalancedTree.make FOLogic.mk_conj
+                 Balanced_Tree.make FOLogic.mk_conj
                  (ListPair.map mk_rec_imp (rec_tms, preds)))))
      and mutual_induct_concl =
-      FOLogic.mk_Trueprop(BalancedTree.make FOLogic.mk_conj qconcls);
+      FOLogic.mk_Trueprop (Balanced_Tree.make FOLogic.mk_conj qconcls);
 
      val dummy = if !Ind_Syntax.trace then
                  (writeln ("induct_concl = " ^
diff -r 690f9cccf232 -r 3032c0308019 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/ZF/ind_syntax.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -99,7 +99,7 @@
       fun is_ind arg = (type_of arg = iT)
   in  case List.filter is_ind (args @ cs) of
          []     => @{const 0}
-       | u_args => BalancedTree.make mk_Un u_args
+       | u_args => Balanced_Tree.make mk_Un u_args
   end;