src/Pure/Proof/extraction.ML
changeset 23178 07ba6b58b3d2
parent 22924 17f1d7af43bd
child 24219 e558fe311376
     1.1 --- a/src/Pure/Proof/extraction.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4  
     1.5  fun merge_rules
     1.6    ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
     1.7 -  foldr add_rule {next = next, rs = rs1, net = net} (subtract (op =) rs1 rs2);
     1.8 +  List.foldr add_rule {next = next, rs = rs1, net = net} (subtract (op =) rs1 rs2);
     1.9  
    1.10  fun condrew thy rules procs =
    1.11    let
    1.12 @@ -136,7 +136,7 @@
    1.13    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    1.14    in Abst (a, SOME T, prf_abstract_over t prf) end;
    1.15  
    1.16 -val mkabs = foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
    1.17 +val mkabs = List.foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
    1.18  
    1.19  fun strip_abs 0 t = t
    1.20    | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
    1.21 @@ -145,7 +145,7 @@
    1.22  fun prf_subst_TVars tye =
    1.23    map_proof_terms (subst_TVars tye) (typ_subst_TVars tye);
    1.24  
    1.25 -fun relevant_vars types prop = foldr (fn
    1.26 +fun relevant_vars types prop = List.foldr (fn
    1.27        (Var ((a, i), T), vs) => (case strip_type T of
    1.28          (_, Type (s, _)) => if member (op =) types s then a :: vs else vs
    1.29        | _ => vs)
    1.30 @@ -237,7 +237,7 @@
    1.31      defs, expand, prep} = ExtractionData.get thy;
    1.32    in
    1.33      ExtractionData.put
    1.34 -      {realizes_eqns = foldr add_rule realizes_eqns (map (prep_eq thy) eqns),
    1.35 +      {realizes_eqns = List.foldr add_rule realizes_eqns (map (prep_eq thy) eqns),
    1.36         typeof_eqns = typeof_eqns, types = types, realizers = realizers,
    1.37         defs = defs, expand = expand, prep = prep} thy
    1.38    end
    1.39 @@ -255,7 +255,7 @@
    1.40    in
    1.41      ExtractionData.put
    1.42        {realizes_eqns = realizes_eqns, realizers = realizers,
    1.43 -       typeof_eqns = foldr add_rule typeof_eqns eqns',
    1.44 +       typeof_eqns = List.foldr add_rule typeof_eqns eqns',
    1.45         types = types, defs = defs, expand = expand, prep = prep} thy
    1.46    end
    1.47  
    1.48 @@ -324,7 +324,7 @@
    1.49          (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
    1.50            (Const ("realizes", T --> propT --> propT) $
    1.51              (if T = nullT then t else list_comb (t, vars')) $ prop);
    1.52 -      val r = foldr forall_intr r' (map (get_var_type r') vars);
    1.53 +      val r = List.foldr forall_intr r' (map (get_var_type r') vars);
    1.54        val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
    1.55      in (name, (vs, (t, prf))) end
    1.56    end;
    1.57 @@ -474,7 +474,7 @@
    1.58              end
    1.59            else (vs', tye)
    1.60  
    1.61 -      in foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
    1.62 +      in List.foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
    1.63  
    1.64      fun find (vs: string list) = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
    1.65      fun find' s = map snd o List.filter (equal s o fst)
    1.66 @@ -569,7 +569,7 @@
    1.67                      val (defs'', corr_prf) =
    1.68                        corr (d + 1) defs' vs' [] [] [] prf' prf' NONE;
    1.69                      val corr_prop = Reconstruct.prop_of corr_prf;
    1.70 -                    val corr_prf' = foldr forall_intr_prf
    1.71 +                    val corr_prf' = List.foldr forall_intr_prf
    1.72                        (proof_combt
    1.73                           (PThm (corr_name name vs', corr_prf, corr_prop,
    1.74                               SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop))
    1.75 @@ -678,7 +678,7 @@
    1.76                             PAxm (cname ^ "_def", eqn,
    1.77                               SOME (map TVar (term_tvars eqn))))) %% corr_prf;
    1.78                      val corr_prop = Reconstruct.prop_of corr_prf';
    1.79 -                    val corr_prf'' = foldr forall_intr_prf
    1.80 +                    val corr_prf'' = List.foldr forall_intr_prf
    1.81                        (proof_combt
    1.82                          (PThm (corr_name s vs', corr_prf', corr_prop,
    1.83                            SOME (map TVar (term_tvars corr_prop))),  vfs_of corr_prop))