# HG changeset patch
# User blanchet
# Date 1377205402 -7200
# Node ID c4e41658307a38675952f4dde839b0ed1c9e112d
# Parent  c898409d8630990627fea0f193ed47af4d6e142e
fixed pattern matching

diff -r c898409d8630 -r c4e41658307a src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Aug 22 23:03:21 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Aug 22 23:03:22 2013 +0200
@@ -179,7 +179,7 @@
       | FastforceM => "fastforce"
       | ForceM => "force"
       | ArithM => "arith"
-      | Blast => "blast"
+      | BlastM => "blast"
       | _ => raise Fail "Sledgehammer_Print: by_method")
 
     fun using_facts [] [] = ""