src/Pure/Isar/specification.ML

                 Position.str_of (Name.pos_of b));
           in (b, mx) end);
     val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
         (var, ((Name.map_name (suffix "_raw") name, []), rhs));
     val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
-        ((name, Code.add_default_eqn_attr :: atts), [prove lthy2 th]);
+        ((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
 
     val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
     val _ =
       if not do_print then ()
       else print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];