# HG changeset patch
# User haftmann
# Date 1282127208 -7200
# Node ID de7984a7172b34860f5c0d8ecfbf709390d9cf50
# Parent  bd9c4e8281ecbd58e2f501136600f5c1aebd3092
deglobalization

diff -r bd9c4e8281ec -r de7984a7172b NEWS
--- a/NEWS	Wed Aug 18 12:19:27 2010 +0200
+++ b/NEWS	Wed Aug 18 12:26:48 2010 +0200
@@ -131,6 +131,16 @@
 similar to inductive_cases.
 
 
+*** FOL ***
+
+* All constant names are now qualified.  INCOMPATIBILITY.
+
+
+*** ZF ***
+
+* All constant names are now qualified.  INCOMPATIBILITY.
+
+
 *** ML ***
 
 * ML antiquotations @{theory} and @{theory_ref} refer to named
diff -r bd9c4e8281ec -r de7984a7172b src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Wed Aug 18 12:19:27 2010 +0200
+++ b/src/FOL/IFOL.thy	Wed Aug 18 12:26:48 2010 +0200
@@ -28,8 +28,6 @@
 
 setup PureThy.old_appl_syntax_setup
 
-global
-
 classes "term"
 default_sort "term"
 
@@ -87,8 +85,6 @@
   Ex        (binder "\<exists>" 10) and
   Ex1       (binder "\<exists>!" 10)
 
-local
-
 finalconsts
   False All Ex
   "op ="
diff -r bd9c4e8281ec -r de7984a7172b src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Wed Aug 18 12:19:27 2010 +0200
+++ b/src/FOLP/IFOLP.thy	Wed Aug 18 12:26:48 2010 +0200
@@ -12,8 +12,6 @@
 
 setup PureThy.old_appl_syntax_setup
 
-global
-
 classes "term"
 default_sort "term"
 
@@ -63,8 +61,6 @@
  nrm            :: p
  NRM            :: p
 
-local
-
 syntax "_Proof" :: "[p,o]=>prop"    ("(_ /: _)" [51, 10] 5)
 
 ML {*
diff -r bd9c4e8281ec -r de7984a7172b src/ZF/Datatype_ZF.thy
--- a/src/ZF/Datatype_ZF.thy	Wed Aug 18 12:19:27 2010 +0200
+++ b/src/ZF/Datatype_ZF.thy	Wed Aug 18 12:26:48 2010 +0200
@@ -61,7 +61,7 @@
 struct
   val trace = Unsynchronized.ref false;
 
-  fun mk_new ([],[]) = Const("True",FOLogic.oT)
+  fun mk_new ([],[]) = Const(@{const_name True},FOLogic.oT)
     | mk_new (largs,rargs) =
         Balanced_Tree.make FOLogic.mk_conj
                  (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
@@ -85,7 +85,7 @@
            if #big_rec_name lcon_info = #big_rec_name rcon_info
                andalso not (null (#free_iffs lcon_info)) then
                if lname = rname then mk_new (largs, rargs)
-               else Const("False",FOLogic.oT)
+               else Const(@{const_name False},FOLogic.oT)
            else raise Match
        val _ =
          if !trace then writeln ("NEW = " ^ Syntax.string_of_term_global sg new)
diff -r bd9c4e8281ec -r de7984a7172b src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Wed Aug 18 12:19:27 2010 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Wed Aug 18 12:26:48 2010 +0200
@@ -118,7 +118,7 @@
 fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
   let
     (*analyze the LHS of a case equation to get a constructor*)
-    fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
+    fun const_of (Const(@{const_name "op ="}, _) $ (_ $ c) $ _) = c
       | const_of eqn = error ("Ill-formed case equation: " ^
                               Syntax.string_of_term_global thy eqn);
 
diff -r bd9c4e8281ec -r de7984a7172b src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Wed Aug 18 12:19:27 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Wed Aug 18 12:26:48 2010 +0200
@@ -102,7 +102,7 @@
 
   val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
 
-  fun dest_tprop (Const("Trueprop",_) $ P) = P
+  fun dest_tprop (Const(@{const_name Trueprop},_) $ P) = P
     | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
                             Syntax.string_of_term ctxt Q);
 
diff -r bd9c4e8281ec -r de7984a7172b src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Wed Aug 18 12:19:27 2010 +0200
+++ b/src/ZF/Tools/typechk.ML	Wed Aug 18 12:26:48 2010 +0200
@@ -75,7 +75,7 @@
          if length rls <= maxr then resolve_tac rls i else no_tac
       end);
 
-fun is_rigid_elem (Const("Trueprop",_) $ (Const(@{const_name mem},_) $ a $ _)) =
+fun is_rigid_elem (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) =
       not (is_Var (head_of a))
   | is_rigid_elem _ = false;