note_thmss: refrain from closing the derivation here;
authorwenzelm
Thu, 30 Nov 2006 16:48:41 +0100
changeset 21612 52859439959a
parent 21611 fc95ff1fe738
child 21613 ae3bb930b50f
note_thmss: refrain from closing the derivation here;
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 =