# HG changeset patch
# User smolkas
# Date 1373542400 -7200
# Node ID 760a567f1609f97de76d6ea80052b6e4b5f65ad0
# Parent  02713cd2c2cd32840b49c822bd72e193b7bdd813
made SML/NJ happy

diff -r 02713cd2c2cd -r 760a567f1609 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Thu Jul 11 13:33:19 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Thu Jul 11 13:33:20 2013 +0200
@@ -119,7 +119,8 @@
 (* PRE CONDITION: the proof must be labeled canocially, see
    Slegehammer_Proof.relabel_proof_canonically *)
 fun compress_proof isar_compress isar_compress_degree merge_timeout_slack
-  { get_time, set_time, preplay_quietly, preplay_fail, ... } proof =
+  ({get_time, set_time, preplay_quietly, preplay_fail, ...} : preplay_interface)
+  proof =
   if isar_compress <= 1.0 then
     proof
   else