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