src/Pure/Isar/specification.ML

         bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
     val (_, ctxt') = lthy |> prep_vars raw_fixes |-> Proof_Context.add_fixes;
 
     val facts' = facts
       |> Attrib.partial_evaluation ctxt'
-      |> Element.facts_map (Element.transform_ctxt (Proof_Context.export_morphism ctxt' lthy));
+      |> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy);
     val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
     val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
   in (res, lthy') end;
 
 in