global "prems" is legacy feature;
authorwenzelm
Fri Jan 14 16:01:29 2011 +0100 (2011-01-14)
changeset 41552c5e71fee3617
parent 41551 791b139a6c1e
child 41553 ccfc070e8157
global "prems" is legacy feature;
src/Pure/assumption.ML
     1.1 --- a/src/Pure/assumption.ML	Fri Jan 14 16:00:11 2011 +0100
     1.2 +++ b/src/Pure/assumption.ML	Fri Jan 14 16:01:29 2011 +0100
     1.3 @@ -79,10 +79,12 @@
     1.4  fun extra_hyps ctxt th =
     1.5    subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
     1.6  
     1.7 -(*named prems -- legacy feature*)
     1.8  val _ = Context.>>
     1.9    (Context.map_theory (Global_Theory.add_thms_dynamic (Binding.name "prems",
    1.10 -    fn Context.Theory _ => [] | Context.Proof ctxt => all_prems_of ctxt)));
    1.11 +    fn Context.Theory _ => []
    1.12 +     | Context.Proof ctxt =>
    1.13 +        (legacy_feature ("Use of global prems" ^ Position.str_of (Position.thread_data ()));
    1.14 +          all_prems_of ctxt))));
    1.15  
    1.16  
    1.17  (* local assumptions *)