--- a/NEWS Wed Feb 15 20:56:30 2012 +0100
+++ b/NEWS Wed Feb 15 21:08:27 2012 +0100
@@ -39,6 +39,10 @@
*** Pure ***
+* Discontinued old "prems" fact, which used to refer to the accidental
+collection of foundational premises in the context (marked as legacy
+since Isabelle2011).
+
* Obsolete command 'types' has been discontinued. Use 'type_synonym'
instead. INCOMPATIBILITY.
--- 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 *)