| changeset 11652 | b2d27a80b0d0 |
| parent 11615 | ca7be12b2cbc |
| child 11715 | 592923615f77 |
--- 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 ****)