src/Pure/assumption.ML
changeset 26435 bdce320cd426
parent 26392 748b263f0e40
child 26463 9283b4185fdf
equal deleted inserted replaced
26434:d004b791218e 26435:bdce320cd426
    76 fun extra_hyps ctxt th = subtract (op aconv) (map Thm.term_of (assms_of ctxt)) (Thm.hyps_of th);
    76 fun extra_hyps ctxt th = subtract (op aconv) (map Thm.term_of (assms_of ctxt)) (Thm.hyps_of th);
    77 
    77 
    78 
    78 
    79 (* named prems -- legacy feature *)
    79 (* named prems -- legacy feature *)
    80 
    80 
    81 val _ = Context.add_setup
    81 val _ = Context.>>
    82   (PureThy.add_thms_dynamic ("prems",
    82   (PureThy.add_thms_dynamic ("prems",
    83     fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt));
    83     fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt));
    84 
    84 
    85 
    85 
    86 (* add assumptions *)
    86 (* add assumptions *)