src/HOL/Tools/datatype_realizer.ML
changeset 30190 479806475f3c
parent 29579 cb520b766e00
child 30280 eb98b49ef835
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sun Mar 01 16:48:06 2009 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sun Mar 01 23:36:12 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Tools/datatype_realizer.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Stefan Berghofer, TU Muenchen
     1.7  
     1.8  Porgram extraction from proofs involving datatypes:
     1.9 @@ -57,8 +56,8 @@
    1.10      fun mk_all i s T t =
    1.11        if i mem is then list_all_free ([(s, T)], t) else t;
    1.12  
    1.13 -    val (prems, rec_fns) = split_list (List.concat (snd (foldl_map
    1.14 -      (fn (j, ((i, (_, _, constrs)), T)) => foldl_map (fn (j, (cname, cargs)) =>
    1.15 +    val (prems, rec_fns) = split_list (List.concat (snd (Library.foldl_map
    1.16 +      (fn (j, ((i, (_, _, constrs)), T)) => Library.foldl_map (fn (j, (cname, cargs)) =>
    1.17          let
    1.18            val Ts = map (typ_of_dtyp descr sorts) cargs;
    1.19            val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
    1.20 @@ -139,8 +138,8 @@
    1.21        tname_of (body_type T) mem ["set", "bool"]) ivs);
    1.22      val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;
    1.23  
    1.24 -    val prf = foldr forall_intr_prf
    1.25 -     (foldr (fn ((f, p), prf) =>
    1.26 +    val prf = List.foldr forall_intr_prf
    1.27 +     (List.foldr (fn ((f, p), prf) =>
    1.28          (case head_of (strip_abs_body f) of
    1.29             Free (s, T) =>
    1.30               let val T' = Logic.varifyT T
    1.31 @@ -151,7 +150,7 @@
    1.32             (Proofterm.proof_combP
    1.33               (prf_of thm', map PBound (length prems - 1 downto 0))) (rec_fns ~~ prems_of thm)) ivs2;
    1.34  
    1.35 -    val r' = if null is then r else Logic.varify (foldr (uncurry lambda)
    1.36 +    val r' = if null is then r else Logic.varify (List.foldr (uncurry lambda)
    1.37        r (map Logic.unvarify ivs1 @ filter_out is_unit
    1.38            (map (head_of o strip_abs_body) rec_fns)));
    1.39  
    1.40 @@ -201,7 +200,7 @@
    1.41  
    1.42      val P = Var (("P", 0), rT' --> HOLogic.boolT);
    1.43      val prf = forall_intr_prf (y, forall_intr_prf (P,
    1.44 -      foldr (fn ((p, r), prf) =>
    1.45 +      List.foldr (fn ((p, r), prf) =>
    1.46          forall_intr_prf (Logic.legacy_varify r, AbsP ("H", SOME (Logic.varify p),
    1.47            prf))) (Proofterm.proof_combP (prf_of thm',
    1.48              map PBound (length prems - 1 downto 0))) (prems ~~ rs)));