--- a/src/HOL/Tools/SMT/verit_replay.ML Mon Mar 28 17:16:42 2022 +0200
+++ b/src/HOL/Tools/SMT/verit_replay.ML Tue Mar 29 12:55:25 2022 +0200
@@ -137,9 +137,9 @@
val args = map (Term.subst_free concl_tranformation o subst_only_free global_transformation) args
val insts = Symtab.map (K (Term.subst_free concl_tranformation o subst_only_free global_transformation)) insts
val proof_prems =
- if Verit_Replay_Methods.requires_subproof_assms prems rule then proof_prems else []
+ if Lethe_Replay_Methods.requires_subproof_assms prems rule then proof_prems else []
val local_inputs =
- if Verit_Replay_Methods.requires_local_input prems rule then input @ inputs else []
+ if Lethe_Replay_Methods.requires_local_input prems rule then input @ inputs else []
val replay = Timing.timing (replay_thm Verit_Replay_Methods.method_for rewrite_rules ll_defs
ctxt assumed [] (proof_prems @ local_inputs) (nthms @ nthms') concl_tranformation
global_transformation args insts)