--- a/src/Pure/proofterm.ML Fri May 21 21:23:37 2004 +0200
+++ b/src/Pure/proofterm.ML Fri May 21 21:24:22 2004 +0200
@@ -104,7 +104,7 @@
val add_prf_rrules : (proof * proof) list -> theory -> theory
val add_prf_rprocs : (string * (Term.typ list -> proof -> proof option)) list ->
theory -> theory
- val rewrite_proof : Type.type_sig -> (proof * proof) list *
+ val rewrite_proof : Type.tsig -> (proof * proof) list *
(string * (typ list -> proof -> proof option)) list -> proof -> proof
val rewrite_proof_notypes : (proof * proof) list *
(string * (typ list -> proof -> proof option)) list -> proof -> proof