diff -r 9c64a52ae499 -r 87ddf7eddfc9 src/HOL/Tools/Sledgehammer/sledgehammer_isar_Reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_Reconstruct.ML	Wed Nov 28 12:22:17 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_Reconstruct.ML	Wed Nov 28 12:23:44 2012 +0100
@@ -9,7 +9,7 @@
 type label = string * int
 type facts = label list * string list
 
-datatype isar_qualifier = Show | Then | Moreover | Ultimately
+datatype isar_qualifier = Show | Then | Ultimately
 
 datatype isar_step =
   Fix of (string * typ) list |
@@ -43,4 +43,5 @@
            inc (fold (inc o metis_steps_recursive) cases 1)
          | _ => I) proof 0
 
-end
\ No newline at end of file
+
+end