diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Provers/blast.ML	Thu Jan 19 21:22:08 2006 +0100
@@ -79,7 +79,7 @@
   val depth_limit : int ref
   val blast_tac         : claset -> int -> tactic
   val Blast_tac         : int -> tactic
-  val setup             : (theory -> theory) list
+  val setup             : theory -> theory
   (*debugging tools*)
   val stats             : bool ref
   val trace             : bool ref
@@ -1329,7 +1329,7 @@
   | blast_meth (SOME lim) = Data.cla_meth' (fn cs => depth_tac cs lim);
 
 val setup =
- [Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]];
+  Method.add_methods [("blast", blast_args blast_meth, "tableau prover")];
 
 
 end;