changeset 69593 | 3dda49e08b9d |
parent 62922 | 96691631c1eb |
child 69605 | a96320074298 |
--- 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>