bang_facts: warning;
authorwenzelm
Fri May 11 00:43:46 2007 +0200 (2007-05-11)
changeset 2293253005f898665
parent 22931 11cc1ccad58e
child 22933 338c7890c96f
bang_facts: warning;
src/Pure/Isar/args.ML
     1.1 --- a/src/Pure/Isar/args.ML	Fri May 11 00:43:45 2007 +0200
     1.2 +++ b/src/Pure/Isar/args.ML	Fri May 11 00:43:46 2007 +0200
     1.3 @@ -340,7 +340,8 @@
     1.4    nat >> PureThy.Single));
     1.5  
     1.6  val bang_facts = Scan.peek (fn context =>
     1.7 -  $$$ "!" >> K (Assumption.prems_of (Context.proof_of context)) || Scan.succeed []);
     1.8 +  $$$ "!" >> (fn _ => (warning "use of prems in proof method";
     1.9 +    Assumption.prems_of (Context.proof_of context))) || Scan.succeed []);
    1.10  
    1.11  
    1.12  (* goal specification *)