src/Pure/Isar/specification.ML

       |> prep_statement attrib prep_stmt elems raw_concl;
     val atts = more_atts @ map attrib raw_atts;
 
     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
             Local_Theory.notes_kind kind
               (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;