changeset 42440 | 5e7a7343ab11 |
parent 42375 | 774df7c59508 |
child 42482 | 42c7ef050bc3 |
--- a/src/Pure/Isar/specification.ML Wed Apr 20 22:57:29 2011 +0200 +++ b/src/Pure/Isar/specification.ML Thu Apr 21 12:56:27 2011 +0200 @@ -227,7 +227,7 @@ val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]); val ([(def_name, [th'])], lthy4) = lthy3 - |> Local_Theory.notes_kind Thm.definitionK + |> Local_Theory.notes_kind "" [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])]; val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;