# HG changeset patch
# User wenzelm
# Date 1150565869 -7200
# Node ID f035261fb5b9bfa30937fe5e41552f06209c18a4
# Parent  f552697b2f195b3d2a780a4bfe10e5bcfb4bc60f
added generalize rule;

diff -r f552697b2f19 -r f035261fb5b9 src/Pure/proofterm.ML
--- 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 =