# HG changeset patch
# User wenzelm
# Date 951251941 -3600
# Node ID 32387a2c7749347570fe7a48938264d6ab2c48c9
# Parent  0d8fa545bd5c17f0953e3c520ca5095c9a185c6e
added boolN;

diff -r 0d8fa545bd5c -r 32387a2c7749 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Tue Feb 22 20:16:07 2000 +0100
+++ b/src/HOL/hologic.ML	Tue Feb 22 21:39:01 2000 +0100
@@ -10,6 +10,7 @@
   val termC: class
   val termS: sort
   val termT: typ
+  val boolN: string
   val boolT: typ
   val false_const: term
   val true_const: term
@@ -80,7 +81,8 @@
 
 (* bool and set *)
 
-val boolT = Type ("bool", []);
+val boolN = "bool";
+val boolT = Type (boolN, []);
 
 val true_const =  Const ("True", boolT)
 and false_const = Const ("False", boolT);
@@ -90,6 +92,7 @@
 fun dest_setT (Type ("set", [T])) = T
   | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
 
+
 (* logic *)
 
 val Trueprop = Const ("Trueprop", boolT --> propT);