# HG changeset patch
# User wenzelm
# Date 1206470398 -3600
# Node ID 748b263f0e404cd44c4dd34bf7b357af8a05d1a6
# Parent  6e8aa5a4eb82200e200b6bdb1de5dad1ff672c7d
setup for dynamic "prems" (legacy);

diff -r 6e8aa5a4eb82 -r 748b263f0e40 src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Tue Mar 25 19:39:57 2008 +0100
+++ b/src/Pure/assumption.ML	Tue Mar 25 19:39:58 2008 +0100
@@ -76,6 +76,13 @@
 fun extra_hyps ctxt th = subtract (op aconv) (map Thm.term_of (assms_of ctxt)) (Thm.hyps_of th);
 
 
+(* named prems -- legacy feature *)
+
+val _ = Context.add_setup
+  (PureThy.add_thms_dynamic ("prems",
+    fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt));
+
+
 (* add assumptions *)
 
 fun add_assms export new_asms =