1.1 --- a/src/Pure/Isar/specification.ML	Thu Nov 30 14:17:22 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Thu Nov 30 14:17:25 2006 +0100
     1.3 @@ -273,7 +273,9 @@
     1.4        prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;
     1.5  
     1.6      fun after_qed' results goal_ctxt' =
     1.7 -      let val results' = burrow (ProofContext.export_standard goal_ctxt' lthy) results in
     1.8 +      let val results' =
     1.9 +        burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results
    1.10 +      in
    1.11          lthy
    1.12          |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
    1.13          |> (fn (res, lthy') =>