# HG changeset patch
# User wenzelm
# Date 1570654812 -7200
# Node ID a74ab9230cb3e17f66373e02847adab5a4f12db9
# Parent  a6644dfe8e260d70b6fe2b6074fa63a3595d353f
tuned;

diff -r a6644dfe8e26 -r a74ab9230cb3 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Oct 09 22:52:34 2019 +0200
+++ b/src/Pure/proofterm.ML	Wed Oct 09 23:00:12 2019 +0200
@@ -1862,9 +1862,8 @@
     val env' = solve thy cs' env
   in thawf (norm_proof env' prf) end handle MIN_PROOF () => MinProof;
 
-fun prop_of_atom prop Ts = subst_atomic_types
-  (map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts)
-  (forall_intr_vfs prop);
+fun prop_of_atom prop Ts =
+  subst_atomic_types (type_variables_of prop ~~ Ts) (forall_intr_vfs prop);
 
 val head_norm = Envir.head_norm Envir.init;