--- 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) =>