--- a/src/Pure/Pure.thy Wed Feb 27 16:27:44 2013 +0100
+++ b/src/Pure/Pure.thy Wed Feb 27 17:32:17 2013 +0100
@@ -29,7 +29,7 @@
"abbreviation" "type_notation" "no_type_notation" "notation"
"no_notation" "axiomatization" "theorems" "lemmas" "declare"
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
- and "use" "ML" :: thy_decl % "ML"
+ and "ML" :: thy_decl % "ML"
and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *)
and "ML_val" "ML_command" :: diag % "ML"
and "setup" "local_setup" "attribute_setup" "method_setup"