# HG changeset patch
# User wenzelm
# Date 1329336507 -3600
# Node ID 7e69b9f3149f3943034348a2338985f28c8bb5ba
# Parent  bf96ed9e55c1d054bedabedd04e6200754406f1a
discontinued obsolete "prems" fact;

diff -r bf96ed9e55c1 -r 7e69b9f3149f NEWS
--- 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.
 
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 *)