setup for dynamic "prems" (legacy);
authorwenzelm
Tue Mar 25 19:39:58 2008 +0100 (2008-03-25)
changeset 26392748b263f0e40
parent 26391 6e8aa5a4eb82
child 26393 42febbed5460
setup for dynamic "prems" (legacy);
src/Pure/assumption.ML
     1.1 --- a/src/Pure/assumption.ML	Tue Mar 25 19:39:57 2008 +0100
     1.2 +++ b/src/Pure/assumption.ML	Tue Mar 25 19:39:58 2008 +0100
     1.3 @@ -76,6 +76,13 @@
     1.4  fun extra_hyps ctxt th = subtract (op aconv) (map Thm.term_of (assms_of ctxt)) (Thm.hyps_of th);
     1.5  
     1.6  
     1.7 +(* named prems -- legacy feature *)
     1.8 +
     1.9 +val _ = Context.add_setup
    1.10 +  (PureThy.add_thms_dynamic ("prems",
    1.11 +    fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt));
    1.12 +
    1.13 +
    1.14  (* add assumptions *)
    1.15  
    1.16  fun add_assms export new_asms =