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