Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Theory.add_typedecls;
authorwenzelm
Fri, 17 Jun 2005 18:33:32 +0200
changeset 16447 01c4b30f91e9
parent 16446 0ab34b9d1b1f
child 16448 6c45c5416b79
Theory.add_typedecls; Sign.local_path;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle