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