--- a/src/Pure/Isar/calculation.ML Wed Dec 10 13:45:44 2014 +0100
+++ b/src/Pure/Isar/calculation.ML Wed Dec 10 17:55:31 2014 +0100
@@ -111,7 +111,13 @@
(** proof commands **)
fun assert_sane final =
- if final then Proof.assert_forward else Proof.assert_forward_or_chain;
+ if final then Proof.assert_forward
+ else
+ Proof.assert_forward_or_chain #>
+ tap (fn state =>
+ if can Proof.assert_chain state then
+ Context_Position.report (Proof.context_of state) (Position.thread_data ()) Markup.improper
+ else ());
fun maintain_calculation int final calc state =
let