# HG changeset patch
# User wenzelm
# Date 1571232661 -7200
# Node ID de6f137a07d3d03d599c236c914cb7c0aa80540c
# Parent  ca7831201a7a56803e353856a0f049a531fe0c3f
tuned -- more stable type inference;

diff -r ca7831201a7a -r de6f137a07d3 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Oct 16 12:42:09 2019 +0200
+++ b/src/Pure/proofterm.ML	Wed Oct 16 15:31:01 2019 +0200
@@ -2242,7 +2242,7 @@
 
 in
 
-val thm_proof = prepare_thm_proof false;
+fun thm_proof thy = prepare_thm_proof false thy;
 
 fun unconstrain_thm_proof thy classrel_proof arity_proof shyps concl promises body =
   prepare_thm_proof true thy classrel_proof arity_proof ("", Position.none)