--- a/src/Pure/simplifier.ML Thu May 18 15:34:01 2023 +0200
+++ b/src/Pure/simplifier.ML Thu May 18 17:21:29 2023 +0200
@@ -128,7 +128,8 @@
val ctxt' = fold Proof_Context.augment lhss ctxt;
val lhss' = Variable.export_terms ctxt' ctxt lhss;
in
- cert_simproc (Proof_Context.theory_of ctxt) name {lhss = lhss', proc = proc}
+ cert_simproc (Proof_Context.theory_of ctxt) name
+ {lhss = lhss', proc = Morphism.entity proc}
end;
local
@@ -311,8 +312,8 @@
val add_del =
(Args.del -- Args.colon >> K (op delsimprocs) ||
Scan.option (Args.add -- Args.colon) >> K (op addsimprocs))
- >> (fn f => fn simproc => fn phi => Thm.declaration_attribute
- (K (Raw_Simplifier.map_ss (fn ctxt => f (ctxt, [transform_simproc phi simproc])))));
+ >> (fn f => fn simproc => Morphism.entity (fn phi => Thm.declaration_attribute
+ (K (Raw_Simplifier.map_ss (fn ctxt => f (ctxt, [transform_simproc phi simproc]))))));
in