src/Pure/simplifier.ML

 val define_simproc_cmd = def_simproc Syntax.read_terms;
 
 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 **)
 
 fun pretty_simpset verbose ctxt =
   let