--- a/src/Pure/Isar/proof_context.ML Tue Mar 18 11:27:09 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML Tue Mar 18 12:25:17 2014 +0100
@@ -1204,8 +1204,9 @@
fun check_case ctxt (name, pos) fxs =
let
- val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, _), _)) =
+ val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, is_proper), _)) =
Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
+ val _ = if is_proper then () else Context_Position.report ctxt pos Markup.improper;
fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
| replace [] ys = ys