--- a/src/HOL/Extraction.thy Sat Oct 12 15:41:59 2019 +0200
+++ b/src/HOL/Extraction.thy Sat Oct 12 16:46:33 2019 +0200
@@ -8,8 +8,6 @@
imports Option
begin
-ML_file \<open>Tools/rewrite_hol_proof.ML\<close>
-
subsection \<open>Setup\<close>
setup \<open>
--- a/src/HOL/HOL.thy Sat Oct 12 15:41:59 2019 +0200
+++ b/src/HOL/HOL.thy Sat Oct 12 16:46:33 2019 +0200
@@ -777,6 +777,7 @@
subsection \<open>Package setup\<close>
ML_file \<open>Tools/hologic.ML\<close>
+ML_file \<open>Tools/rewrite_hol_proof.ML\<close>
subsubsection \<open>Sledgehammer setup\<close>
--- a/src/HOL/Tools/rewrite_hol_proof.ML Sat Oct 12 15:41:59 2019 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Sat Oct 12 16:46:33 2019 +0200
@@ -310,8 +310,8 @@
| strip_cong ps (PThm ({name = "HOL.refl", ...}, _) % SOME f %% _) = SOME (f, ps)
| strip_cong _ _ = NONE;
-val subst_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of subst))));
-val sym_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of sym))));
+val subst_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of @{thm subst}))));
+val sym_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of@{thm sym}))));
fun make_subst Ts prf xs (_, []) = prf
| make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) =