src/Pure/Isar/specification.ML

--- a/src/Pure/Isar/specification.ML	Fri May 09 21:03:44 2014 +0200
+++ b/src/Pure/Isar/specification.ML	Fri May 09 22:04:50 2014 +0200
@@ -223,7 +223,9 @@
 
     val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
 
-    val _ = Proof_Display.print_consts int lthy4 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
+    val _ =
+      Proof_Display.print_consts int (Position.thread_data ()) lthy4
+        (member (op =) (Term.add_frees lhs' [])) [(x, T)];
   in ((lhs, (def_name, th')), lthy4) end;
 
 val definition' = gen_def check_free_spec;
@@ -256,7 +258,7 @@
       |> Local_Theory.abbrev mode (var, rhs) |> snd
       |> Proof_Context.restore_syntax_mode lthy;
 
-    val _ = Proof_Display.print_consts int lthy2 (K false) [(x, T)];
+    val _ = Proof_Display.print_consts int (Position.thread_data ()) lthy2 (K false) [(x, T)];
   in lthy2 end;
 
 val abbreviation = gen_abbrev check_free_spec;
@@ -301,7 +303,7 @@
       |> Attrib.partial_evaluation ctxt'
       |> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy);
     val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
-    val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
+    val _ = Proof_Display.print_results int (Position.thread_data ()) lthy' ((kind, ""), res);
   in (res, lthy') end;
 
 in
@@ -389,6 +391,7 @@
       |> prep_statement (prep_att lthy) prep_stmt elems raw_concl;
     val atts = more_atts @ map (prep_att lthy) raw_atts;
 
+    val pos = Position.thread_data ();
     fun after_qed' results goal_ctxt' =
       let
         val results' =
@@ -400,12 +403,12 @@
               (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
         val lthy'' =
           if Attrib.is_empty_binding (name, atts) then
-            (Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
+            (Proof_Display.print_results int pos lthy' ((kind, ""), res); lthy')
           else
             let
               val ([(res_name, _)], lthy'') =
                 Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
-              val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
+              val _ = Proof_Display.print_results int pos lthy' ((kind, res_name), res);
             in lthy'' end;
       in after_qed results' lthy'' end;
   in