# HG changeset patch # User wenzelm # Date 1164901721 -3600 # Node ID 52859439959a779520db58d181a6931c20c69d16 # Parent fc95ff1fe7382b09e6610f7d44c35e4cb5b70770 note_thmss: refrain from closing the derivation here; diff -r fc95ff1fe738 -r 52859439959a src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Nov 30 14:17:37 2006 +0100 +++ b/src/Pure/Isar/proof_context.ML Thu Nov 30 16:48:41 2006 +0100 @@ -794,7 +794,8 @@ 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 =