--- a/src/Pure/Isar/specification.ML Thu Aug 21 13:46:29 2014 +0200
+++ b/src/Pure/Isar/specification.ML Thu Aug 21 22:48:39 2014 +0200
@@ -301,7 +301,7 @@
val facts' = facts
|> Attrib.partial_evaluation ctxt'
- |> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy);
+ |> Attrib.transform_facts (Proof_Context.export_morphism ctxt' lthy);
val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
val _ = Proof_Display.print_results int (Position.thread_data ()) lthy' ((kind, ""), res);
in (res, lthy') end;