diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Extraction.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -22,7 +22,7 @@
       Proofterm.rewrite_proof thy
         (RewriteHOLProof.rews,
          ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class ctxt]) o
-      ProofRewriteRules.elim_vars (curry Const @{const_name default})
+      ProofRewriteRules.elim_vars (curry Const \<^const_name>\<open>default\<close>)
     end)
 \<close>