src/Pure/Proof/proof_rewrite_rules.ML
changeset 13646 46ed3d042ba5
parent 13608 9a6f43b8eae1
child 13917 a67c9e6570ac
     1.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 11 12:47:52 2002 +0200
     1.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Mon Oct 14 10:44:32 2002 +0200
     1.3 @@ -249,7 +249,7 @@
     1.4          val thms = flat (map (fn (s, ps) =>
     1.5              if s mem defnames then []
     1.6              else map (pair s o Some o fst) (filter_out (fn (p, _) =>
     1.7 -              null (add_term_consts (p, []) inter cnames)) ps))
     1.8 +              null (term_consts p inter cnames)) ps))
     1.9            (Symtab.dest (thms_of_proof Symtab.empty prf)))
    1.10        in Reconstruct.expand_proof sign thms end
    1.11    in