# HG changeset patch
# User paulson
# Date 1002102324 -7200
# Node ID b2d27a80b0d08e0420bbaa20a079bc3601d9ad92
# Parent  201b3f76c7b72c2c37e9c2c24ec684186e717a71
eta-expansion required for SML/NJ

diff -r 201b3f76c7b7 -r b2d27a80b0d0 src/Pure/proofterm.ML
--- 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 ****)