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

diff -r bd6359ed1636 -r dc92eee56ed7 NEWS
--- a/NEWS	Thu Aug 19 16:03:07 2010 +0200
+++ b/NEWS	Thu Aug 19 16:08:53 2010 +0200
@@ -86,9 +86,18 @@
 * Some previously unqualified names have been qualified:
 
   types
+    bool ~> HOL.bool
     nat ~> Nat.nat
 
   constants
+    Trueprop ~> HOL.Trueprop
+    True ~> HOL.True
+    False ~> HOL.False
+    Not ~> HOL.Not
+    The ~> HOL.The
+    All ~> HOL.All
+    Ex ~> HOL.Ex
+    Ex1 ~> HOL.Ex1
     Let ~> HOL.Let
     If ~> HOL.If
     Ball ~> Set.Ball
diff -r bd6359ed1636 -r dc92eee56ed7 src/HOL/Import/HOL/bool.imp
--- a/src/HOL/Import/HOL/bool.imp	Thu Aug 19 16:03:07 2010 +0200
+++ b/src/HOL/Import/HOL/bool.imp	Thu Aug 19 16:08:53 2010 +0200
@@ -12,11 +12,11 @@
   "ARB" > "ARB_def"
 
 const_maps
-  "~" > "Not"
+  "~" > "HOL.Not"
   "bool_case" > "Datatype.bool.bool_case"
   "\\/" > "op |"
   "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
-  "T" > "True"
+  "T" > "HOL.True"
   "RES_SELECT" > "HOL4Base.bool.RES_SELECT"
   "RES_FORALL" > "HOL4Base.bool.RES_FORALL"
   "RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE"
@@ -25,13 +25,13 @@
   "ONE_ONE" > "HOL4Setup.ONE_ONE"
   "LET" > "HOL4Compat.LET"
   "IN" > "HOL4Base.bool.IN"
-  "F" > "False"
+  "F" > "HOL.False"
   "COND" > "HOL.If"
   "ARB" > "HOL4Base.bool.ARB"
-  "?!" > "Ex1"
-  "?" > "Ex"
+  "?!" > "HOL.Ex1"
+  "?" > "HOL.Ex"
   "/\\" > "op &"
-  "!" > "All"
+  "!" > "HOL.All"
 
 thm_maps
   "bool_case_thm" > "HOL4Base.bool.bool_case_thm"
diff -r bd6359ed1636 -r dc92eee56ed7 src/HOL/Import/HOLLight/hollight.imp
--- a/src/HOL/Import/HOLLight/hollight.imp	Thu Aug 19 16:03:07 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp	Thu Aug 19 16:08:53 2010 +0200
@@ -18,13 +18,13 @@
   "finite_sum" > "HOLLight.hollight.finite_sum"
   "finite_image" > "HOLLight.hollight.finite_image"
   "cart" > "HOLLight.hollight.cart"
-  "bool" > "bool"
+  "bool" > "HOL.bool"
   "N_3" > "HOLLight.hollight.N_3"
   "N_2" > "HOLLight.hollight.N_2"
   "N_1" > "Product_Type.unit"
 
 const_maps
-  "~" > "Not"
+  "~" > "HOL.Not"
   "two_2" > "HOLLight.hollight.two_2"
   "two_1" > "HOLLight.hollight.two_1"
   "treal_of_num" > "HOLLight.hollight.treal_of_num"
@@ -229,8 +229,8 @@
   "ALL2" > "HOLLight.hollight.ALL2"
   "ABS_prod" > "Abs_Prod"
   "@" > "Hilbert_Choice.Eps"
-  "?!" > "Ex1"
-  "?" > "Ex"
+  "?!" > "HOL.Ex1"
+  "?" > "HOL.Ex"
   ">=" > "HOLLight.hollight.>="
   ">" > "HOLLight.hollight.>"
   "==>" > "op -->"
@@ -243,7 +243,7 @@
   "+" > "Groups.plus" :: "nat => nat => nat"
   "*" > "Groups.times" :: "nat => nat => nat"
   "$" > "HOLLight.hollight.$"
-  "!" > "All"
+  "!" > "HOL.All"
 
 const_renames
   "ALL" > "ALL_list"
diff -r bd6359ed1636 -r dc92eee56ed7 src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Thu Aug 19 16:03:07 2010 +0200
+++ b/src/HOL/Import/hol4rews.ML	Thu Aug 19 16:08:53 2010 +0200
@@ -616,7 +616,7 @@
     fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "=="}, _],_,_]] = x
       | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax all}, _],_]] = x
       | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "==>"}, _],_,_]] = x
-      | handle_meta [x] = Appl[Constant "Trueprop",x]
+      | handle_meta [x] = Appl[Constant @{const_syntax Trueprop}, x]
       | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
 in
 val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)]