# HG changeset patch
# User wenzelm
# Date 1119026012 -7200
# Node ID 01c4b30f91e9f8944dd2bb06c323f683c0ebf1f4
# Parent  0ab34b9d1b1f101ea931d3a72e8c3fce433418ce
Theory.add_typedecls;
Sign.local_path;

diff -r 0ab34b9d1b1f -r 01c4b30f91e9 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Jun 17 18:33:31 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Jun 17 18:33:32 2005 +0200
@@ -97,7 +97,7 @@
 val typedeclP =
   OuterSyntax.command "typedecl" "type declaration" K.thy_decl
     (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
-      Toplevel.theory (PureThy.add_typedecls [(a, args, mx)])));
+      Toplevel.theory (Theory.add_typedecls [(a, args, mx)])));
 
 val typeabbrP =
   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
@@ -221,11 +221,11 @@
 
 val globalP =
   OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl
-    (Scan.succeed (Toplevel.theory PureThy.global_path));
+    (Scan.succeed (Toplevel.theory Sign.root_path));
 
 val localP =
   OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
-    (Scan.succeed (Toplevel.theory PureThy.local_path));
+    (Scan.succeed (Toplevel.theory Sign.local_path));
 
 val hideP =
   OuterSyntax.command "hide" "hide names from given name space" K.thy_decl