src/Pure/Isar/specification.ML
changeset 28370 37f56e6e702d
parent 28114 2637fb838f74
child 28703 aef727ef30e5
     1.1 --- a/src/Pure/Isar/specification.ML	Fri Sep 26 09:09:53 2008 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Fri Sep 26 09:10:02 2008 +0200
     1.3 @@ -184,7 +184,7 @@
     1.4      val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
     1.5          (var, ((Name.map_name (suffix "_raw") name, []), rhs));
     1.6      val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
     1.7 -        ((name, Code.add_default_func_attr :: atts), [prove lthy2 th]);
     1.8 +        ((name, Code.add_default_eqn_attr :: atts), [prove lthy2 th]);
     1.9  
    1.10      val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
    1.11      val _ =