--- a/src/Pure/Isar/specification.ML Mon Jun 06 21:28:45 2016 +0200
+++ b/src/Pure/Isar/specification.ML Mon Jun 06 21:28:46 2016 +0200
@@ -260,7 +260,7 @@
val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
val ([(def_name, [th'])], lthy4) = lthy3
- |> Local_Theory.notes [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
+ |> Local_Theory.notes [((name, Code.add_default_eqn_attrib Code.Equation :: atts), [([th], [])])];
val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;