Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Proof/proof_rewrite_rules.ML
changeset 13646 46ed3d042ba5
parent 13608 9a6f43b8eae1
child 13917 a67c9e6570ac 
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 11 12:47:52 2002 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Mon Oct 14 10:44:32 2002 +0200
@@ -249,7 +249,7 @@
         val thms = flat (map (fn (s, ps) =>
             if s mem defnames then []
             else map (pair s o Some o fst) (filter_out (fn (p, _) =>
-              null (add_term_consts (p, []) inter cnames)) ps))
+              null (term_consts p inter cnames)) ps))
           (Symtab.dest (thms_of_proof Symtab.empty prf)))
       in Reconstruct.expand_proof sign thms end
   in
isabelle