# HG changeset patch
# User wenzelm
# Date 1467744662 -7200
# Node ID ae07cd27ebf1886877b950315be77d1247613edd
# Parent  734723445a8cc1a617d9cca15954a62810b48f45
PIDE reports of implicit variable scope;

diff -r 734723445a8c -r ae07cd27ebf1 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Jul 05 14:20:27 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Tue Jul 05 20:51:02 2016 +0200
@@ -122,7 +122,12 @@
   in ((vars, xs), ctxt'') end;
 
 fun close_form ctxt ys prems concl =
-  let val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) (rev ys));
+  let
+    val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) (rev ys));
+
+    val pos_props = Logic.strip_imp_concl concl :: Logic.strip_imp_prems concl @ prems;
+    fun get_pos x = maps (get_positions ctxt x) pos_props;
+    val _ = Context_Position.reports ctxt (maps (Syntax_Phases.reports_of_scope o get_pos) xs);
   in Logic.close_prop_constraint (Variable.default_type ctxt) (xs ~~ xs) prems concl end;
 
 fun dummy_frees ctxt xs tss =