src/Pure/Isar/instance.ML

     fun define def ctxt =
       let
         val def' = (apsnd o apsnd) (Syntax.check_prop ctxt) def;
       in Specification.definition def' ctxt end;
     val _ = if not (null defs) then Output.legacy_feature
-      "Instance command with attached attached definitions; use instantiation instead." else ();
+      "Instance command with attached definitions; use instantiation instead." else ();
   in if not (null defs) orelse forall (Class.is_class thy) sort
   then
     thy
     |> TheoryTarget.instantiation ([tyco], sorts, sort)
     |> `(fn ctxt => map (mk_def ctxt) defs)