src/Pure/Proof/proof_rewrite_rules.ML
changeset 17018 1e9e0f5877f2
parent 16861 7446b4be013b
child 17137 0f48fbb60a61
     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' [])