--- a/src/Pure/simplifier.ML Wed Apr 22 19:22:43 2020 +0200
+++ b/src/Pure/simplifier.ML Tue Apr 21 07:28:17 2020 +0000
@@ -158,6 +158,34 @@
end;
+(** congruence rule to protect foundational terms of local definitions **)
+
+local
+
+fun make_cong ctxt = Thm.close_derivation \<^here> o Thm.reflexive
+ o Thm.cterm_of ctxt o Logic.varify_global o list_comb;
+
+fun add_cong (const_binding, (const, target_params)) gthy =
+ if null target_params
+ then gthy
+ else
+ let
+ val cong = make_cong (Context.proof_of gthy) (const, target_params)
+ val cong_binding = Binding.qualify_name true const_binding "cong"
+ in
+ gthy
+ |> Attrib.generic_notes Thm.theoremK
+ [((cong_binding, []), [([cong], [])])]
+ |> snd
+ end;
+
+in
+
+val _ = Theory.setup (Generic_Target.add_foundation_interpretation add_cong);
+
+end;
+
+
(** pretty_simpset **)