1.1 --- a/NEWS	Wed Feb 15 20:56:30 2012 +0100
     1.2 +++ b/NEWS	Wed Feb 15 21:08:27 2012 +0100
     1.3 @@ -39,6 +39,10 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Discontinued old "prems" fact, which used to refer to the accidental
     1.8 +collection of foundational premises in the context (marked as legacy
     1.9 +since Isabelle2011).
    1.10 +
    1.11  * Obsolete command 'types' has been discontinued.  Use 'type_synonym'
    1.12  instead.  INCOMPATIBILITY.
    1.13  

     2.1 --- a/src/Pure/assumption.ML	Wed Feb 15 20:56:30 2012 +0100
     2.2 +++ b/src/Pure/assumption.ML	Wed Feb 15 21:08:27 2012 +0100
     2.3 @@ -79,13 +79,6 @@
     2.4  fun extra_hyps ctxt th =
     2.5    subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
     2.6  
     2.7 -val _ = Context.>>
     2.8 -  (Context.map_theory (Global_Theory.add_thms_dynamic (Binding.name "prems",
     2.9 -    fn Context.Theory _ => []
    2.10 -     | Context.Proof ctxt =>
    2.11 -        (legacy_feature ("Use of global prems" ^ Position.str_of (Position.thread_data ()));
    2.12 -          all_prems_of ctxt))));
    2.13 -
    2.14  
    2.15  (* local assumptions *)
    2.16