diff -r 196bd0305c0d -r 37f56e6e702d src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Fri Sep 26 09:09:53 2008 +0200 +++ b/src/Pure/Isar/specification.ML Fri Sep 26 09:10:02 2008 +0200 @@ -184,7 +184,7 @@ 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_func_attr :: atts), [prove lthy2 th]); + ((name, Code.add_default_eqn_attr :: atts), [prove lthy2 th]); val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs; val _ =