# HG changeset patch
# User wenzelm
# Date 901638334 -7200
# Node ID 54aaa779b6b4516de45ff6686afc21b297c7e94f
# Parent  a69fe5a61b6cb59654a8e86b8317ec0030b6c98b
removed global_names flag;

diff -r a69fe5a61b6c -r 54aaa779b6b4 src/CTT/ROOT.ML
--- a/src/CTT/ROOT.ML	Tue Jul 28 17:03:12 1998 +0200
+++ b/src/CTT/ROOT.ML	Tue Jul 28 17:05:34 1998 +0200
@@ -10,8 +10,6 @@
 val banner = "Constructive Type Theory";
 writeln banner;
 
-reset global_names;
-
 print_depth 1;  
 
 use_thy "CTT";
diff -r a69fe5a61b6c -r 54aaa779b6b4 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Tue Jul 28 17:03:12 1998 +0200
+++ b/src/HOL/Record.thy	Tue Jul 28 17:05:34 1998 +0200
@@ -42,12 +42,8 @@
 
 (* type class for record extensions *)
 
-global          (*compatibility with global_names flag!*)
-
 axclass more < term
 
-local
-
 instance unit :: more
 instance "*" :: (term, more) more
 
diff -r a69fe5a61b6c -r 54aaa779b6b4 src/HOL/TLA/ROOT.ML
--- a/src/HOL/TLA/ROOT.ML	Tue Jul 28 17:03:12 1998 +0200
+++ b/src/HOL/TLA/ROOT.ML	Tue Jul 28 17:05:34 1998 +0200
@@ -12,8 +12,6 @@
 *)
 Syntax.ambiguity_level := 10000;
 
-reset global_names;
-
 (*FIXME: the old auto_tac is sometimes needed!*)
 fun old_auto_tac (cs,ss) = 
     let val cs' = cs addss ss 
diff -r a69fe5a61b6c -r 54aaa779b6b4 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Jul 28 17:03:12 1998 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue Jul 28 17:05:34 1998 +0200
@@ -99,7 +99,7 @@
 
 (* more type class *)
 
-val moreS = ["more"];
+val moreS = ["Record.more"];
 
 
 (* types *)
diff -r a69fe5a61b6c -r 54aaa779b6b4 src/HOLCF/IMP/ROOT.ML
--- a/src/HOLCF/IMP/ROOT.ML	Tue Jul 28 17:03:12 1998 +0200
+++ b/src/HOLCF/IMP/ROOT.ML	Tue Jul 28 17:05:34 1998 +0200
@@ -4,8 +4,6 @@
     Copyright   1997  TU Muenchen
 *)
 
-reset global_names;
-
 (*Load theories from ../meta_theory without generating HTML files
   (has already been done by HOL/IMP/ROOT.ML)*)
 val old_make_html = !make_html;
diff -r a69fe5a61b6c -r 54aaa779b6b4 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Jul 28 17:03:12 1998 +0200
+++ b/src/Pure/pure_thy.ML	Tue Jul 28 17:05:34 1998 +0200
@@ -12,7 +12,6 @@
   val get_thm: theory -> xstring -> thm
   val get_thms: theory -> xstring -> thm list
   val thms_of: theory -> (string * thm) list
-  val global_names: bool ref
   structure ProtoPure:
     sig
       val thy: theory
@@ -313,15 +312,10 @@
 
 (* control prefixing of theory name *)
 
-(*compatibility flag, likely to disappear someday*)
-val global_names = ref false;
-
-fun global_path thy =
-  if ! global_names then thy else Theory.root_path thy;
+val global_path = Theory.root_path;
 
 fun local_path thy =
-  if ! global_names then thy
-  else thy |> Theory.root_path |> Theory.add_path (get_name thy);
+  thy |> Theory.root_path |> Theory.add_path (get_name thy);
 
 
 (* begin / end theory *)
diff -r a69fe5a61b6c -r 54aaa779b6b4 src/Sequents/ROOT.ML
--- a/src/Sequents/ROOT.ML	Tue Jul 28 17:03:12 1998 +0200
+++ b/src/Sequents/ROOT.ML	Tue Jul 28 17:05:34 1998 +0200
@@ -9,8 +9,6 @@
 val banner = "Sequent Calculii";
 writeln banner;
 
-reset global_names;
-
 print_depth 1;  
 
 use_thy "Sequents";