# HG changeset patch
# User blanchet
# Date 1272531359 -7200
# Node ID 3c2438efe22463e9392147d02373ee3de7678993
# Parent  81dc2c20f05287ba91fd951dbe294574513f6192
make SML/NJ happy, take 2

diff -r 81dc2c20f052 -r 3c2438efe224 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 10:25:26 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 10:55:59 2010 +0200
@@ -955,7 +955,8 @@
         |> the_default "Warning: The Isar proof construction failed.\n"
   in (one_line_proof ^ isar_proof, lemma_names) end
 
-fun proof_text isar_proof isar_params =
-  if isar_proof then isar_proof_text isar_params else metis_proof_text
+fun proof_text isar_proof isar_params other_params =
+  (if isar_proof then isar_proof_text isar_params else metis_proof_text)
+      other_params
 
 end;