diff -r 0850d43cb355 -r 71fc3776c453 src/Pure/Pure.thy
--- 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"