Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bang_facts: warning;
authorwenzelm
Fri, 11 May 2007 00:43:46 +0200
changeset 22932 53005f898665
parent 22931 11cc1ccad58e
child 22933 338c7890c96f
bang_facts: warning;
src/Pure/Isar/args.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle