--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Feb 14 15:27:10 2013 +0100
@@ -193,9 +193,9 @@
(* FIXME: Ad hoc list *)
val technical_prefixes =
- ["ATP", "Code_Evaluation", "Datatype", "DSequence", "Enum", "Lazy_Sequence",
- "Meson", "Metis", "Nitpick", "New_DSequence", "New_Random_Sequence",
- "Quickcheck", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
+ ["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence",
+ "Limited_Sequence", "Meson", "Metis", "Nitpick",
+ "Quickcheck_Random", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
"Random_Sequence", "Sledgehammer", "SMT"]
|> map (suffix Long_Name.separator)