Adapted to new interface of thms_of_proof.
authorberghofe
Wed Aug 03 16:25:22 2005 +0200 (2005-08-03)
changeset 170181e9e0f5877f2
parent 17017 fa8e32209734
child 17019 f68598628d08
Adapted to new interface of thms_of_proof.
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Aug 03 16:24:52 2005 +0200
     1.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Aug 03 16:25:22 2005 +0200
     1.3 @@ -247,7 +247,7 @@
     1.4              if s mem defnames then []
     1.5              else map (pair s o SOME o fst) (filter_out (fn (p, _) =>
     1.6                null (term_consts p inter cnames)) ps))
     1.7 -          (Symtab.dest (thms_of_proof Symtab.empty prf)))
     1.8 +          (Symtab.dest (thms_of_proof prf Symtab.empty)))
     1.9        in Reconstruct.expand_proof sign thms end
    1.10    in
    1.11      rewrite_terms (Pattern.rewrite_term tsig defs' [])
     2.1 --- a/src/Pure/proof_general.ML	Wed Aug 03 16:24:52 2005 +0200
     2.2 +++ b/src/Pure/proof_general.ML	Wed Aug 03 16:25:22 2005 +0200
     2.3 @@ -495,8 +495,8 @@
     2.4    let
     2.5      val names = filter_out (equal "") (map Thm.name_of_thm ths);
     2.6      val deps = filter_out (equal "")
     2.7 -      (Symtab.keys (Library.foldl (uncurry Proofterm.thms_of_proof)
     2.8 -        (Symtab.empty, map Thm.proof_of ths)));
     2.9 +      (Symtab.keys (fold Proofterm.thms_of_proof
    2.10 +        (map Thm.proof_of ths) Symtab.empty));
    2.11    in
    2.12      if null names orelse null deps then ()
    2.13      else thm_deps_message (spaces_quote names, spaces_quote deps)