# HG changeset patch
# User wenzelm
# Date 1178837026 -7200
# Node ID 53005f89866571f746f276c716fa3000e934c032
# Parent  11cc1ccad58e46f48ffef051c67033d1d888c37e
bang_facts: warning;

diff -r 11cc1ccad58e -r 53005f898665 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Fri May 11 00:43:45 2007 +0200
+++ b/src/Pure/Isar/args.ML	Fri May 11 00:43:46 2007 +0200
@@ -340,7 +340,8 @@
   nat >> PureThy.Single));
 
 val bang_facts = Scan.peek (fn context =>
-  $$$ "!" >> K (Assumption.prems_of (Context.proof_of context)) || Scan.succeed []);
+  $$$ "!" >> (fn _ => (warning "use of prems in proof method";
+    Assumption.prems_of (Context.proof_of context))) || Scan.succeed []);
 
 
 (* goal specification *)