src/Pure/Isar/specification.ML
changeset 58028 e4250d370657
parent 58011 bc6bced136e5
child 58848 fd0c85d7da38
--- 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;