src/Provers/blast.ML
changeset 30722 623d4831c8cf
parent 30609 983e8b6e4e69
child 31945 d5f186aa0bed
--- a/src/Provers/blast.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/Provers/blast.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -1302,14 +1302,13 @@
 
 (** method setup **)
 
-val blast_method =
-  Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
-  Method.sections Data.cla_modifiers >>
-  (fn (prems, NONE) => Data.cla_meth' blast_tac prems
-    | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems);
-
 val setup =
   setup_depth_limit #>
-  Method.setup @{binding blast} blast_method "tableau prover";
+  Method.setup @{binding blast}
+    (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
+      Method.sections Data.cla_modifiers >>
+      (fn (prems, NONE) => Data.cla_meth' blast_tac prems
+        | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems))
+    "classical tableau prover";
 
 end;