src/HOL/Tools/datatype_realizer.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 16123 1381e90c2694
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -144,8 +144,8 @@
     1.4        tname_of (body_type T) mem ["set", "bool"]) ivs);
     1.5      val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (assoc (rvs, ixn)))) ivs;
     1.6  
     1.7 -    val prf = Library.foldr forall_intr_prf (ivs2,
     1.8 -      Library.foldr (fn ((f, p), prf) =>
     1.9 +    val prf = foldr forall_intr_prf
    1.10 +     (foldr (fn ((f, p), prf) =>
    1.11          (case head_of (strip_abs_body f) of
    1.12             Free (s, T) =>
    1.13               let val T' = Type.varifyT T
    1.14 @@ -153,12 +153,12 @@
    1.15                 (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
    1.16               end
    1.17           | _ => AbsP ("H", SOME p, prf)))
    1.18 -           (rec_fns ~~ prems_of thm, Proofterm.proof_combP
    1.19 -             (prf_of thm', map PBound (length prems - 1 downto 0))));
    1.20 +           (Proofterm.proof_combP
    1.21 +             (prf_of thm', map PBound (length prems - 1 downto 0))) (rec_fns ~~ prems_of thm)) ivs2;
    1.22  
    1.23 -    val r' = if null is then r else Logic.varify (Library.foldr (uncurry lambda)
    1.24 -      (map Logic.unvarify ivs1 @ filter_out is_unit
    1.25 -        (map (head_of o strip_abs_body) rec_fns), r));
    1.26 +    val r' = if null is then r else Logic.varify (foldr (uncurry lambda)
    1.27 +      r (map Logic.unvarify ivs1 @ filter_out is_unit
    1.28 +          (map (head_of o strip_abs_body) rec_fns)));
    1.29  
    1.30    in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
    1.31  
    1.32 @@ -209,10 +209,10 @@
    1.33  
    1.34      val P = Var (("P", 0), rT' --> HOLogic.boolT);
    1.35      val prf = forall_intr_prf (y, forall_intr_prf (P,
    1.36 -      Library.foldr (fn ((p, r), prf) =>
    1.37 +      foldr (fn ((p, r), prf) =>
    1.38          forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),
    1.39 -          prf))) (prems ~~ rs, Proofterm.proof_combP (prf_of thm',
    1.40 -            map PBound (length prems - 1 downto 0)))));
    1.41 +          prf))) (Proofterm.proof_combP (prf_of thm',
    1.42 +            map PBound (length prems - 1 downto 0))) (prems ~~ rs)));
    1.43      val r' = Logic.varify (Abs ("y", Type.varifyT T,
    1.44        list_abs (map dest_Free rs, list_comb (r,
    1.45          map Bound ((length rs - 1 downto 0) @ [length rs])))));