--- a/src/Pure/proofterm.ML Sat Jun 17 19:37:48 2006 +0200
+++ b/src/Pure/proofterm.ML Sat Jun 17 19:37:49 2006 +0200
@@ -77,6 +77,7 @@
val freezeT : term -> proof -> proof
val rotate_proof : term list -> term -> int -> proof -> proof
val permute_prems_prf : term list -> int -> int -> proof -> proof
+ val generalize: string list * string list -> int -> proof -> proof
val instantiate : ((indexname * sort) * typ) list * ((indexname * typ) * term) list
-> proof -> proof
val lift_proof : term -> int -> term -> proof -> proof
@@ -653,6 +654,12 @@
end;
+(***** generalization *****)
+
+fun generalize (tfrees, frees) idx prf =
+ map_proof_terms (Term.generalize (tfrees, frees) idx) (Term.generalizeT tfrees idx) prf;
+
+
(***** instantiation *****)
fun instantiate (instT, inst) prf =