tuned signature;

--- a/src/Pure/proofterm.ML	Fri Nov 01 11:29:40 2019 +0100
+++ b/src/Pure/proofterm.ML	Fri Nov 01 14:30:22 2019 +0100
@@ -153,6 +153,8 @@
   val add_prf_rrule: proof * proof -> theory -> theory
   val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) -> theory -> theory
   val set_preproc: (theory -> proof -> proof) -> theory -> theory
+  val forall_intr_variables_term: term -> term
+  val forall_intr_variables: term -> proof -> proof
   val no_skel: proof
   val normal_skel: proof
   val rewrite_proof: theory -> (proof * proof) list *
@@ -1633,10 +1635,10 @@
 
 (** reconstruction of partial proof terms **)
 
-local
+fun forall_intr_variables_term prop = fold_rev Logic.all (variables_of prop) prop;
+fun forall_intr_variables prop prf = fold_rev forall_intr_proof' (variables_of prop) prf;
 
-fun forall_intr_vfs prop = fold_rev Logic.all (variables_of prop) prop;
-fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof' (variables_of prop) prf;
+local
 
 fun app_types shift prop Ts prf =
   let
@@ -1762,7 +1764,7 @@
                 NONE => fold_map (mk_tvar o Type.sort_of_atyp) prop_types env
               | SOME Ts => (Ts, env));
             val prop' = subst_atomic_types (prop_types ~~ Ts)
-              (forall_intr_vfs prop) handle ListPair.UnequalLengths =>
+              (forall_intr_variables_term prop) handle ListPair.UnequalLengths =>
                 error ("Wrong number of type arguments for " ^ quote (guess_name prf))
           in (prop', change_types (SOME Ts) prf, [], env', vTs) end;
 
@@ -1922,7 +1924,7 @@
   in thawf (norm_proof env' prf) end handle MIN_PROOF () => MinProof;
 
 fun prop_of_atom prop Ts =
-  subst_atomic_types (type_variables_of prop ~~ Ts) (forall_intr_vfs prop);
+  subst_atomic_types (type_variables_of prop ~~ Ts) (forall_intr_variables_term prop);
 
 val head_norm = Envir.head_norm Envir.init;
 
@@ -1981,7 +1983,7 @@
                             val prf1 =
                               thm_body_proof_open thm_body
                               |> reconstruct_proof thy prop
-                              |> forall_intr_vfs_prf prop;
+                              |> forall_intr_variables prop;
                             val (seen1, maxidx1, prf2) = expand_init seen prf1
                             val seen2 = seen1 |> Inttab.update (serial, (maxidx1, prf2));
                           in (seen2, maxidx1, prf2) end