# HG changeset patch
# User wenzelm
# Date 1440948770 -7200
# Node ID 62f3b498827791c898f3579e62181b84a0fb997b
# Parent  ed0a1067b1df3dce3bb62868124b3935d50774c5
tuned;

diff -r ed0a1067b1df -r 62f3b4988277 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Aug 30 17:32:36 2015 +0200
+++ b/src/Pure/thm.ML	Sun Aug 30 17:32:50 2015 +0200
@@ -1196,8 +1196,8 @@
         val Thm (der, {cert, hyps, shyps, tpairs, prop, ...}) = th;
         val (inst', (instT', (cert', shyps'))) =
           (cert, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT
-            handle CONTEXT (msg, cTs, cts, ths, NONE) =>
-              raise CONTEXT (msg, cTs, cts, th :: ths, NONE);
+            handle CONTEXT (msg, cTs, cts, ths, context) =>
+              raise CONTEXT (msg, cTs, cts, th :: ths, context);
         val subst = Term_Subst.instantiate_maxidx (instT', inst');
         val (prop', maxidx1) = subst prop ~1;
         val (tpairs', maxidx') =