--- 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;