tuned -- more stable type inference;

--- 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)