diff -r bf96ed9e55c1 -r 7e69b9f3149f src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Wed Feb 15 20:56:30 2012 +0100
+++ b/src/Pure/assumption.ML	Wed Feb 15 21:08:27 2012 +0100
@@ -79,13 +79,6 @@
 fun extra_hyps ctxt th =
   subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
 
-val _ = Context.>>
-  (Context.map_theory (Global_Theory.add_thms_dynamic (Binding.name "prems",
-    fn Context.Theory _ => []
-     | Context.Proof ctxt =>
-        (legacy_feature ("Use of global prems" ^ Position.str_of (Position.thread_data ()));
-          all_prems_of ctxt))));
-
 
 (* local assumptions *)