src/Pure/Isar/proof_context.ML

 local
 
 fun gen_note_thmss get k = fold_map (fn ((bname, more_attrs), raw_facts) => fn ctxt =>
   let
     val stmt = is_stmt ctxt;
-    val kind = if stmt then [] else [PureThy.kind k];
+(*    val kind = if stmt then [] else [PureThy.kind k];  *)
+    val kind = [];   (* FIXME refrain from closing the derivation here *)
 
     val facts = map (apfst (get ctxt)) raw_facts;
     fun app (th, attrs) x =
       swap (foldl_map (Thm.proof_attributes (attrs @ more_attrs @ kind)) (x, th));
     val (res, ctxt') = fold_map app facts ctxt;