src/Pure/Isar/specification.ML

       in ((prems, stmt, facts), goal_ctxt) end);
 
 fun gen_theorem prep_att prep_stmt
     kind before_qed after_qed (name, raw_atts) raw_elems raw_concl lthy0 =
   let
-    val _ = LocalTheory.assert lthy0;
+    val _ = LocalTheory.affirm lthy0;
     val thy = ProofContext.theory_of lthy0;
 
     val (loc, ctxt, lthy) =
       (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
         (SOME loc, true) => (* workaround non-modularity of in/includes *)  (* FIXME *)