--- a/src/Pure/Isar/isar_syn.ML Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML Thu Mar 15 00:10:45 2012 +0100
@@ -18,7 +18,7 @@
"\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
"advanced", "and", "assumes", "attach", "begin", "binder",
"constrains", "defines", "fixes", "for", "identifier", "if",
- "imports", "in", "infix", "infixl", "infixr", "is",
+ "imports", "in", "infix", "infixl", "infixr", "is", "keywords",
"notes", "obtains", "open", "output", "overloaded", "pervasive",
"shows", "structure", "unchecked", "uses", "where", "|"];
@@ -28,12 +28,10 @@
val _ =
Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
- (Thy_Header.args >> (fn (name, imports, uses) =>
+ (Thy_Header.args >> (fn header =>
Toplevel.print o
Toplevel.init_theory
- (fn () =>
- Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ())
- name imports (map (apfst Path.explode) uses))));
+ (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
val _ =
Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)