--- 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;