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 17018 1e9e0f5877f2
parent 16861 7446b4be013b
child 17137 0f48fbb60a61 
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Aug 03 16:24:52 2005 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Aug 03 16:25:22 2005 +0200
@@ -247,7 +247,7 @@
             if s mem defnames then []
             else map (pair s o SOME o fst) (filter_out (fn (p, _) =>
               null (term_consts p inter cnames)) ps))
-          (Symtab.dest (thms_of_proof Symtab.empty prf)))
+          (Symtab.dest (thms_of_proof prf Symtab.empty)))
       in Reconstruct.expand_proof sign thms end
   in
     rewrite_terms (Pattern.rewrite_term tsig defs' [])
isabelle