# HG changeset patch
# User wenzelm
# Date 1295017289 -3600
# Node ID c5e71fee36178267232a9447d360a9e866217218
# Parent  791b139a6c1e24f7c7886758e44088c77bb519de
global "prems" is legacy feature;

diff -r 791b139a6c1e -r c5e71fee3617 src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Fri Jan 14 16:00:11 2011 +0100
+++ b/src/Pure/assumption.ML	Fri Jan 14 16:01:29 2011 +0100
@@ -79,10 +79,12 @@
 fun extra_hyps ctxt th =
   subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
 
-(*named prems -- legacy feature*)
 val _ = Context.>>
   (Context.map_theory (Global_Theory.add_thms_dynamic (Binding.name "prems",
-    fn Context.Theory _ => [] | Context.Proof ctxt => all_prems_of ctxt)));
+    fn Context.Theory _ => []
+     | Context.Proof ctxt =>
+        (legacy_feature ("Use of global prems" ^ Position.str_of (Position.thread_data ()));
+          all_prems_of ctxt))));
 
 
 (* local assumptions *)