--- a/src/Pure/Isar/specification.ML Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Pure/Isar/specification.ML Tue Dec 31 14:29:16 2013 +0100
@@ -391,7 +391,8 @@
fun after_qed' results goal_ctxt' =
let
- val results' = burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results;
+ val results' =
+ burrow (map (Goal.norm_result lthy) o Proof_Context.export goal_ctxt' lthy) results;
val (res, lthy') =
if forall (Attrib.is_empty_binding o fst) stmt then (map (pair "") results', lthy)
else