# HG changeset patch
# User wenzelm
# Date 1570715550 -7200
# Node ID 730251503341e3cee5d9895a2787073caaa57de4
# Parent  63c60df79187cb6ef77cf5c278b2941c81ee8d3e
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);

diff -r 63c60df79187 -r 730251503341 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Oct 10 15:18:40 2019 +0200
+++ b/src/Pure/proofterm.ML	Thu Oct 10 15:52:30 2019 +0200
@@ -112,7 +112,7 @@
   val legacy_freezeT: term -> proof -> proof
   val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof
   val permute_prems_proof: term list -> int -> int -> proof -> proof
-  val generalize: string list * string list -> int -> proof -> proof
+  val generalize_proof: string list * string list -> int -> term -> proof -> proof
   val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
     -> proof -> proof
   val lift_proof: term -> int -> term -> proof -> proof
@@ -950,10 +950,21 @@
 
 (* generalization *)
 
-fun generalize (tfrees, frees) idx =
-  Same.commit (map_proof_terms_same
-    (Term_Subst.generalize_same (tfrees, frees) idx)
-    (Term_Subst.generalizeT_same tfrees idx));
+fun generalize_proof (tfrees, frees) idx prop prf =
+  let
+    val gen =
+      if null frees then []
+      else
+        fold_aterms (fn Free (x, T) => member (op =) frees x ? insert (op =) (x, T) | _ => I)
+          (Term_Subst.generalize (tfrees, []) idx prop) [];
+  in
+    prf
+    |> Same.commit (map_proof_terms_same
+        (Term_Subst.generalize_same (tfrees, []) idx)
+        (Term_Subst.generalizeT_same tfrees idx))
+    |> fold (fn (x, T) => forall_intr_proof (x, Free (x, T)) NONE) gen
+    |> fold_rev (fn (x, T) => fn prf' => prf' %> Var (Name.clean_index (x, idx), T)) gen
+  end;
 
 
 (* instantiation *)
diff -r 63c60df79187 -r 730251503341 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Oct 10 15:18:40 2019 +0200
+++ b/src/Pure/thm.ML	Thu Oct 10 15:52:30 2019 +0200
@@ -1496,12 +1496,12 @@
         val _ = exists bad_term hyps andalso
           raise THM ("generalize: variable free in assumptions", 0, [th]);
 
-        val gen = Term_Subst.generalize (tfrees, frees) idx;
-        val prop' = gen prop;
-        val tpairs' = map (apply2 gen) tpairs;
+        val generalize = Term_Subst.generalize (tfrees, frees) idx;
+        val prop' = generalize prop;
+        val tpairs' = map (apply2 generalize) tpairs;
         val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
       in
-        Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der,
+        Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop) der,
          {cert = cert,
           tags = [],
           maxidx = maxidx',