--- 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 *)