# HG changeset patch
# User paulson
# Date 1131989134 -3600
# Node ID c4f873d656030c9bc854e4c85248985b796c780e
# Parent  73ce773f12de286a9a81644008906702e432c64d
removal of is_hol

diff -r 73ce773f12de -r c4f873d65603 src/FOL/blastdata.ML
--- a/src/FOL/blastdata.ML	Mon Nov 14 16:26:40 2005 +0100
+++ b/src/FOL/blastdata.ML	Mon Nov 14 18:25:34 2005 +0100
@@ -3,7 +3,6 @@
 structure Blast_Data = 
   struct
   type claset	= Cla.claset
-  val is_hol    = false
   val notE	= notE
   val ccontr	= ccontr
   val contr_tac = Cla.contr_tac
diff -r 73ce773f12de -r c4f873d65603 src/HOL/blastdata.ML
--- a/src/HOL/blastdata.ML	Mon Nov 14 16:26:40 2005 +0100
+++ b/src/HOL/blastdata.ML	Mon Nov 14 18:25:34 2005 +0100
@@ -16,7 +16,6 @@
 structure Blast_Data = 
   struct
   type claset	= Classical.claset
-  val is_hol    = true
   val notE	= notE
   val ccontr	= ccontr
   val contr_tac = Classical.contr_tac
diff -r 73ce773f12de -r c4f873d65603 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Mon Nov 14 16:26:40 2005 +0100
+++ b/src/Provers/blast.ML	Mon Nov 14 18:25:34 2005 +0100
@@ -8,6 +8,9 @@
   SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules??
   Needs explicit instantiation of assumptions?
 
+Given the typeargs system, constructor Const could be eliminated, with
+TConst replaced by a constructor that takes the typargs list as an argument.
+However, Const is heavily used for logical connectives.
 
 Blast_tac is often more powerful than fast_tac, but has some limitations.
 Blast_tac...
@@ -48,7 +51,6 @@
   sig
   type claset
   val notE		: thm		(* [| ~P;  P |] ==> R *)
-  val is_hol    : bool      (*Is this HOL or FOL/ZF?*)	
   val ccontr		: thm		
   val contr_tac 	: int -> tactic
   val dup_intr		: thm -> thm
@@ -156,7 +158,11 @@
 fun isGoal (Const"*Goal*" $ _) = true
   | isGoal _                   = false;
 
-val boolT = if Data.is_hol then "bool" else "o";
+val boolT = 
+  case term_vars (hd (prems_of Data.notE)) of
+      [Term.Var(_, Type(s, []))] => s
+    | _ => error ("Theorem notE is ill-formed: " ^ string_of_thm Data.notE);
+
 val Trueprop = Term.Const("Trueprop", Type(boolT,[])-->propT);
 fun mk_tprop P = Term.$ (Trueprop, P);