1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Jun 17 18:33:31 2005 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Jun 17 18:33:32 2005 +0200
     1.3 @@ -97,7 +97,7 @@
     1.4  val typedeclP =
     1.5    OuterSyntax.command "typedecl" "type declaration" K.thy_decl
     1.6      (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
     1.7 -      Toplevel.theory (PureThy.add_typedecls [(a, args, mx)])));
     1.8 +      Toplevel.theory (Theory.add_typedecls [(a, args, mx)])));
     1.9  
    1.10  val typeabbrP =
    1.11    OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
    1.12 @@ -221,11 +221,11 @@
    1.13  
    1.14  val globalP =
    1.15    OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl
    1.16 -    (Scan.succeed (Toplevel.theory PureThy.global_path));
    1.17 +    (Scan.succeed (Toplevel.theory Sign.root_path));
    1.18  
    1.19  val localP =
    1.20    OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
    1.21 -    (Scan.succeed (Toplevel.theory PureThy.local_path));
    1.22 +    (Scan.succeed (Toplevel.theory Sign.local_path));
    1.23  
    1.24  val hideP =
    1.25    OuterSyntax.command "hide" "hide names from given name space" K.thy_decl