# HG changeset patch
# User blanchet
# Date 1272358299 -7200
# Node ID 69004340f53ce8a051a8daf68ca926a034625e5c
# Parent  9459be72b89eb293c7d9fee4f073d5d547ad42a6
fix SML/NJ compilation (I hope)

diff -r 9459be72b89e -r 69004340f53c src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Apr 27 10:42:41 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Apr 27 10:51:39 2010 +0200
@@ -863,7 +863,7 @@
         |> the_default "Warning: The Isar proof construction failed.\n"
   in (one_line_proof ^ isar_proof, lemma_names) end
 
-fun proof_text isar_proof =
-  if isar_proof then isar_proof_text else K metis_proof_text
+fun proof_text isar_proof isar_params =
+  if isar_proof then isar_proof_text isar_params else metis_proof_text
 
 end;