--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 24 15:29:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 24 16:24:11 2010 +0200
@@ -613,8 +613,8 @@
"Try this command: " ^
Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "."
fun minimize_line _ [] = ""
- | minimize_line minimize_command facts =
- case minimize_command facts of
+ | minimize_line minimize_command ss =
+ case minimize_command ss of
"" => ""
| command =>
"\nTo minimize the number of lemmas, try this: " ^