src/Pure/Isar/interpretation.ML

 
 fun meta_rewrite eqns ctxt = (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
 
 fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
   let
-    val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
+    val facts = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
       :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
     val (eqns', ctxt') = ctxt
       |> note Thm.theoremK facts
       |-> meta_rewrite;
     val dep_morphs = map2 (fn (dep, morph) => fn wits =>