fixed pattern matching
authorblanchet
Thu, 22 Aug 2013 23:03:22 +0200
changeset 53149 c4e41658307a
parent 53148 c898409d8630
child 53150 5565d1b56f84
fixed pattern matching
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 [] [] = ""