src/Pure/Pure.thy
changeset 58918 8d36bc5eaed3
parent 58868 c5e1cce7ace3
child 58928 23d0ffd48006
--- a/src/Pure/Pure.thy	Wed Nov 05 22:39:49 2014 +0100
+++ b/src/Pure/Pure.thy	Thu Nov 06 11:44:41 2014 +0100
@@ -13,7 +13,6 @@
     "identifier" "if" "imports" "in" "includes" "infix" "infixl"
     "infixr" "is" "keywords" "notes" "obtains" "open" "output"
     "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
-  and "theory" :: thy_begin % "theory"
   and "header" :: heading
   and "chapter" :: heading
   and "section" :: heading
@@ -27,7 +26,7 @@
     "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_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" ?? *)