--- a/src/Pure/Pure.thy Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Pure/Pure.thy Sat Apr 19 17:23:05 2014 +0200
@@ -14,7 +14,6 @@
"infixr" "is" "keywords" "notes" "obtains" "open" "output"
"overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
and "theory" :: thy_begin % "theory"
- and "SML_file" "ML_file" :: thy_load % "ML"
and "header" :: diag
and "chapter" :: thy_heading1
and "section" :: thy_heading2
@@ -30,6 +29,8 @@
"definition" "abbreviation" "type_notation" "no_type_notation" "notation"
"no_notation" "axiomatization" "theorems" "lemmas" "declare"
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
+ and "SML_file" "ML_file" :: thy_load % "ML"
+ and "SML_import" "SML_export" :: thy_decl % "ML"
and "ML" :: thy_decl % "ML"
and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *)
and "ML_val" "ML_command" :: diag % "ML"