clarified fact position, notably for reports on literal facts;

--- a/src/Pure/Isar/proof.ML	Mon Jul 04 14:51:19 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Jul 04 19:08:54 2016 +0200
@@ -1097,6 +1097,7 @@
           in (prems, ctxt'') end);
 
     (*result*)
+    val results_bindings = map (apfst Binding.default_pos) shows_bindings;
     fun after_qed' (result_ctxt, results) state' =
       let
         val ctxt' = context_of state';
@@ -1107,7 +1108,7 @@
         val export = map export0 #> Variable.export result_ctxt ctxt';
       in
         state'
-        |> local_results (shows_bindings ~~ burrow export results)
+        |> local_results (results_bindings ~~ burrow export results)
         |-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
         |> after_qed (result_ctxt, results)
       end;