src/HOL/Extraction.thy
changeset 17203 29b2563f5c11
parent 16417 9bc16273c2d4
child 18456 8cc35e95450a
     1.1 --- a/src/HOL/Extraction.thy	Wed Aug 31 15:46:39 2005 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Wed Aug 31 15:46:40 2005 +0200
     1.3 @@ -38,11 +38,11 @@
     1.4    [Extraction.add_types
     1.5        [("bool", ([], NONE)),
     1.6         ("set", ([realizes_set_proc], SOME mk_realizes_set))],
     1.7 -    Extraction.set_preprocessor (fn sg =>
     1.8 +    Extraction.set_preprocessor (fn thy =>
     1.9        Proofterm.rewrite_proof_notypes
    1.10          ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::
    1.11            ProofRewriteRules.rprocs true) o
    1.12 -      Proofterm.rewrite_proof (Sign.tsig_of sg)
    1.13 +      Proofterm.rewrite_proof thy
    1.14          (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
    1.15        ProofRewriteRules.elim_vars (curry Const "arbitrary"))]
    1.16  end