# HG changeset patch
# User haftmann
# Date 1282226587 -7200
# Node ID bd6359ed16368e2293f867fcef28911622931cbd
# Parent  f8999e19dd49541c63f0758f3e101a40816e22e8
deglobalized named HOL constants

diff -r f8999e19dd49 -r bd6359ed1636 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Aug 19 16:03:01 2010 +0200
+++ b/src/HOL/HOL.thy	Thu Aug 19 16:03:07 2010 +0200
@@ -47,8 +47,6 @@
   "fun" :: (type, type) type
   itself :: (type) type
 
-global
-
 typedecl bool
 
 judgment
@@ -58,19 +56,20 @@
   True          :: bool
   False         :: bool
   Not           :: "bool => bool"                   ("~ _" [40] 40)
+
+global consts
   "op &"        :: "[bool, bool] => bool"           (infixr "&" 35)
   "op |"        :: "[bool, bool] => bool"           (infixr "|" 30)
   "op -->"      :: "[bool, bool] => bool"           (infixr "-->" 25)
 
   "op ="        :: "['a, 'a] => bool"               (infixl "=" 50)
 
+local consts
   The           :: "('a => bool) => 'a"
   All           :: "('a => bool) => bool"           (binder "ALL " 10)
   Ex            :: "('a => bool) => bool"           (binder "EX " 10)
   Ex1           :: "('a => bool) => bool"           (binder "EX! " 10)
 
-local
-
 
 subsubsection {* Additional concrete syntax *}
 
@@ -1575,7 +1574,7 @@
   val atomize_conjL = @{thm atomize_conjL}
   val atomize_disjL = @{thm atomize_disjL}
   val operator_names =
-    [@{const_name "op |"}, @{const_name "op &"}, @{const_name "Ex"}]
+    [@{const_name "op |"}, @{const_name "op &"}, @{const_name Ex}]
 );
 *}
 
diff -r f8999e19dd49 -r bd6359ed1636 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Thu Aug 19 16:03:01 2010 +0200
+++ b/src/HOL/Tools/hologic.ML	Thu Aug 19 16:03:07 2010 +0200
@@ -143,15 +143,15 @@
 
 (* bool and set *)
 
-val boolN = "bool";
+val boolN = "HOL.bool";
 val boolT = Type (boolN, []);
 
-val true_const =  Const ("True", boolT);
-val false_const = Const ("False", boolT);
+val true_const =  Const ("HOL.True", boolT);
+val false_const = Const ("HOL.False", boolT);
 
 fun mk_setT T = T --> boolT;
 
-fun dest_setT (Type ("fun", [T, Type ("bool", [])])) = T
+fun dest_setT (Type ("fun", [T, Type ("HOL.bool", [])])) = T
   | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
 
 fun mk_set T ts =
@@ -181,11 +181,11 @@
 
 (* logic *)
 
-val Trueprop = Const ("Trueprop", boolT --> propT);
+val Trueprop = Const ("HOL.Trueprop", boolT --> propT);
 
 fun mk_Trueprop P = Trueprop $ P;
 
-fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
+fun dest_Trueprop (Const ("HOL.Trueprop", _) $ P) = P
   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
 
 fun conj_intr thP thQ =
@@ -233,7 +233,7 @@
 fun dest_imp (Const ("op -->", _) $ A $ B) = (A, B)
   | dest_imp  t = raise TERM ("dest_imp", [t]);
 
-fun dest_not (Const ("Not", _) $ t) = t
+fun dest_not (Const ("HOL.Not", _) $ t) = t
   | dest_not t = raise TERM ("dest_not", [t]);
 
 fun eq_const T = Const ("op =", T --> T --> boolT);
@@ -242,11 +242,11 @@
 fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
   | dest_eq t = raise TERM ("dest_eq", [t])
 
-fun all_const T = Const ("All", [T --> boolT] ---> boolT);
+fun all_const T = Const ("HOL.All", [T --> boolT] ---> boolT);
 fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
 fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t;
 
-fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
+fun exists_const T = Const ("HOL.Ex", [T --> boolT] ---> boolT);
 fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
 
 fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);