diff -r 499a63c30d55 -r 96691631c1eb src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Sat Apr 09 12:36:25 2016 +0200
+++ b/src/HOL/Extraction.thy	Sat Apr 09 13:28:32 2016 +0200
@@ -16,12 +16,14 @@
   Extraction.add_types
       [("bool", ([], NONE))] #>
   Extraction.set_preprocessor (fn thy =>
+    let val ctxt = Proof_Context.init_global thy in
       Proofterm.rewrite_proof_notypes
         ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o
       Proofterm.rewrite_proof thy
         (RewriteHOLProof.rews,
-         ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o
-      ProofRewriteRules.elim_vars (curry Const @{const_name default}))
+         ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class ctxt]) o
+      ProofRewriteRules.elim_vars (curry Const @{const_name default})
+    end)
 \<close>
 
 lemmas [extraction_expand] =