# HG changeset patch
# User wenzelm
# Date 1729625384 -7200
# Node ID 7c66656131900d51265d170c8f94c947d643706d
# Parent  b35c2aa05fcffd78dc7e27c6a57f1972bb3d296f
tuned signature;

diff -r b35c2aa05fcf -r 7c6665613190 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Oct 22 20:53:54 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Oct 22 21:29:44 2024 +0200
@@ -95,6 +95,7 @@
   val read_term_schematic: Proof.context -> string -> term
   val read_term_abbrev: Proof.context -> string -> term
   val show_abbrevs: bool Config.T
+  val contract_abbrevs: Proof.context -> term -> term
   val expand_abbrevs: Proof.context -> term -> term
   val cert_term: Proof.context -> term -> term
   val cert_prop: Proof.context -> term -> term