diff -r 165f4e1937f4 -r 27e6d344d724 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Feb 20 15:56:26 2002 +0100
+++ b/src/Pure/proofterm.ML	Wed Feb 20 15:58:38 2002 +0100
@@ -47,6 +47,7 @@
   val add_prf_tfree_names : string list * proof -> string list
   val add_prf_tvar_ixns : indexname list * proof -> indexname list
   val maxidx_of_proof : proof -> int
+  val change_type : typ list option -> proof -> proof
   val prf_abstract_over : term -> proof -> proof
   val prf_incr_bv : int -> int -> int -> int -> proof -> proof
   val incr_pboundvars : int -> int -> proof -> proof
@@ -268,6 +269,11 @@
 fun maxidx_of_proof prf = fold_proof_terms
   (Int.max o apfst maxidx_of_term) (Int.max o apfst maxidx_of_typ) (~1, prf); 
 
+fun change_type opTs (PThm (name, prf, prop, _)) = PThm (name, prf, prop, opTs)
+  | change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs)
+  | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)
+  | change_type _ prf = prf;
+
 
 (***** utilities *****)