src/Pure/Proof/proof_rewrite_rules.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -197,7 +197,7 @@
     1.4          fun strip [] t = t
     1.5            | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
     1.6        in
     1.7 -        strip Ts (foldl (uncurry lambda o Library.swap) (t', frees))
     1.8 +        strip Ts (Library.foldl (uncurry lambda o Library.swap) (t', frees))
     1.9        end;
    1.10  
    1.11      fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2
    1.12 @@ -227,9 +227,9 @@
    1.13                val vs = vars_of prop;
    1.14                val tvars = term_tvars prop;
    1.15                val (_, rhs) = Logic.dest_equals prop;
    1.16 -              val rhs' = foldl betapply (subst_TVars (map fst tvars ~~ Ts)
    1.17 -                (foldr (fn p => Abs ("", dummyT, abstract_over p)) (vs, rhs)),
    1.18 -                map the ts);
    1.19 +              val rhs' = Library.foldl betapply (subst_TVars (map fst tvars ~~ Ts)
    1.20 +                (Library.foldr (fn p => Abs ("", dummyT, abstract_over p)) (vs, rhs)),
    1.21 +                map valOf ts);
    1.22              in
    1.23                change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
    1.24              end
    1.25 @@ -245,7 +245,7 @@
    1.26      val f = if not r then I else
    1.27        let
    1.28          val cnames = map (fst o dest_Const o fst) defs';
    1.29 -        val thms = flat (map (fn (s, ps) =>
    1.30 +        val thms = List.concat (map (fn (s, ps) =>
    1.31              if s mem defnames then []
    1.32              else map (pair s o SOME o fst) (filter_out (fn (p, _) =>
    1.33                null (term_consts p inter cnames)) ps))