# HG changeset patch
# User wenzelm
# Date 1136062181 -3600
# Node ID 45c915f5f58076e1ba412a80334b9bb66ca237f3
# Parent  0347c1bba406db225d20084c187187bb834c708e
explicitly reject consts *Goal*, *False*;

diff -r 0347c1bba406 -r 45c915f5f580 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sat Dec 31 21:49:40 2005 +0100
+++ b/src/Provers/blast.ML	Sat Dec 31 21:49:41 2005 +0100
@@ -1235,9 +1235,15 @@
   in  skoSubgoal 0 (from 0 (discard_foralls t))  end;
 
 
+fun reject_const thy c =
+  if is_some (Sign.const_type thy c) then
+    error ("Blast: theory contains illegal constant " ^ quote c)
+  else ();
+
 fun initialize thy =
-    (fullTrace:=[];  trail := [];  ntrail := 0;
-     nclosed := 0;  ntried := 1;  typargs := Sign.const_typargs thy);
+ (fullTrace:=[];  trail := [];  ntrail := 0;
+  nclosed := 0;  ntried := 1;  typargs := Sign.const_typargs thy;
+  reject_const thy "*Goal*"; reject_const thy "*False*");
 
 
 (*Tactic using tableau engine and proof reconstruction.
@@ -1323,11 +1329,7 @@
   | blast_meth (SOME lim) = Data.cla_meth' (fn cs => depth_tac cs lim);
 
 val setup =
- [fn thy => thy
-    |> Sign.root_path
-    |> Theory.add_consts_i [("*Goal*", propT, NoSyn), ("*False*", propT, NoSyn)]
-    |> Sign.restore_naming thy,
-  Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]];
+ [Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]];
 
 
 end;