eta-expansion required for SML/NJ

--- a/src/Pure/proofterm.ML	Tue Oct 02 20:23:33 2001 +0200
+++ b/src/Pure/proofterm.ML	Wed Oct 03 11:45:24 2001 +0200
@@ -945,7 +945,7 @@
 fun rewrite_proof tsig = rewrite_prf (fn (tab, f) =>
   Type.typ_match tsig (tab, f ()) handle Type.TYPE_MATCH => raise PMatch);
 
-val rewrite_proof_notypes = rewrite_prf fst;
+fun rewrite_proof_notypes tsig = rewrite_prf fst tsig;
 
 (**** theory data ****)