src/ZF/Tools/inductive_package.ML
changeset 32765 3032c0308019
parent 32091 30e2ffbba718
child 32957 675c0c7e6a37
     1.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Sep 29 22:33:27 2009 +0200
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Sep 29 22:48:24 2009 +0200
     1.3 @@ -113,7 +113,7 @@
     1.4          val exfrees = OldTerm.term_frees intr \\ rec_params
     1.5          val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
     1.6      in List.foldr FOLogic.mk_exists
     1.7 -             (BalancedTree.make FOLogic.mk_conj (zeq::prems)) exfrees
     1.8 +             (Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees
     1.9      end;
    1.10  
    1.11    (*The Part(A,h) terms -- compose injections to make h*)
    1.12 @@ -122,7 +122,7 @@
    1.13  
    1.14    (*Access to balanced disjoint sums via injections*)
    1.15    val parts = map mk_Part
    1.16 -    (BalancedTree.accesses {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = Bound 0}
    1.17 +    (Balanced_Tree.accesses {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = Bound 0}
    1.18        (length rec_tms));
    1.19  
    1.20    (*replace each set by the corresponding Part(A,h)*)
    1.21 @@ -130,7 +130,7 @@
    1.22  
    1.23    val fp_abs = absfree(X', iT,
    1.24                     mk_Collect(z', dom_sum,
    1.25 -                              BalancedTree.make FOLogic.mk_disj part_intrs));
    1.26 +                              Balanced_Tree.make FOLogic.mk_disj part_intrs));
    1.27  
    1.28    val fp_rhs = Fp.oper $ dom_sum $ fp_abs
    1.29  
    1.30 @@ -238,7 +238,7 @@
    1.31       DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
    1.32  
    1.33    (*combines disjI1 and disjI2 to get the corresponding nested disjunct...*)
    1.34 -  val mk_disj_rls = BalancedTree.accesses
    1.35 +  val mk_disj_rls = Balanced_Tree.accesses
    1.36      {left = fn rl => rl RS @{thm disjI1},
    1.37       right = fn rl => rl RS @{thm disjI2},
    1.38       init = @{thm asm_rl}};
    1.39 @@ -398,10 +398,10 @@
    1.40             (Ind_Syntax.mk_all_imp
    1.41              (big_rec_tm,
    1.42               Abs("z", Ind_Syntax.iT,
    1.43 -                 BalancedTree.make FOLogic.mk_conj
    1.44 +                 Balanced_Tree.make FOLogic.mk_conj
    1.45                   (ListPair.map mk_rec_imp (rec_tms, preds)))))
    1.46       and mutual_induct_concl =
    1.47 -      FOLogic.mk_Trueprop(BalancedTree.make FOLogic.mk_conj qconcls);
    1.48 +      FOLogic.mk_Trueprop (Balanced_Tree.make FOLogic.mk_conj qconcls);
    1.49  
    1.50       val dummy = if !Ind_Syntax.trace then
    1.51                   (writeln ("induct_concl = " ^