src/Tools/interpretation_with_defs.ML
changeset 47249 c0481c3c2a6c
parent 46961 5c6955f487e5
child 55599 6535c537b243
--- a/src/Tools/interpretation_with_defs.ML	Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Tools/interpretation_with_defs.ML	Sun Apr 01 19:07:32 2012 +0200
@@ -23,7 +23,7 @@
       map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
         maps snd;
   in
-    Element.generic_note_thmss Thm.lemmaK
+    Attrib.generic_notes Thm.lemmaK
       (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
     #-> (fn facts => `(fn context => meta_rewrite context facts))
     #-> (fn eqns => fold (fn ((dep, morph), wits) =>