# HG changeset patch
# User wenzelm
# Date 1570891593 -7200
# Node ID e62d5433bb475ad5ce378d44f95c09f5091ab042
# Parent  3777d9aaaaad33ab25d098a4a83cdb90854e4446
early setup of proof preprocessing;

diff -r 3777d9aaaaad -r e62d5433bb47 src/HOL/Extraction.thy
--- 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>
diff -r 3777d9aaaaad -r e62d5433bb47 src/HOL/HOL.thy
--- 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>
diff -r 3777d9aaaaad -r e62d5433bb47 src/HOL/Tools/rewrite_hol_proof.ML
--- 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) =