# HG changeset patch
# User wenzelm
# Date 1164670526 -3600
# Node ID a0d0ea84521db4ada7fe4bf9e7e576283e43d292
# Parent  a8070c4b6d43f64c47cc848f05571c5189b6de62
simplified '?' operator;
note_thmss: no naming;

diff -r a8070c4b6d43 -r a0d0ea84521d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Nov 28 00:35:25 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Nov 28 00:35:26 2006 +0100
@@ -282,7 +282,7 @@
     val syntax = syntax_of ctxt;
     val consts = consts_of ctxt;
     val t' = t
-      |> K abbrevs ? rewrite_term thy (Consts.abbrevs_of consts (! print_mode @ [""]))
+      |> abbrevs ? rewrite_term thy (Consts.abbrevs_of consts (! print_mode @ [""]))
       |> Sign.extern_term (Consts.extern_early consts) thy
       |> LocalSyntax.extern_term syntax;
   in
@@ -764,8 +764,9 @@
 
 fun lthms_containing ctxt spec =
   FactIndex.find (fact_index_of ctxt) spec
-  |> map ((not o valid_thms ctxt) ? apfst (fn name =>
-    NameSpace.hidden (if name = "" then "unnamed" else name)));
+  |> map (fn (name, ths) =>
+    if valid_thms ctxt (name, ths) then (name, ths)
+    else (NameSpace.hidden (if name = "" then "unnamed" else name), ths));
 
 
 (* name space operations *)
@@ -809,18 +810,14 @@
 
 fun gen_note_thmss get k = fold_map (fn ((bname, more_attrs), raw_facts) => fn ctxt =>
   let
-    val name = full_name ctxt bname;
     val stmt = is_stmt ctxt;
-
     val kind = if stmt then [] else [PureThy.kind k];
-    val facts = raw_facts |> map (apfst (get ctxt))
-      |> (if stmt then I else PureThy.name_thmss name);
 
+    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;
-    val thms = flat res
-      |> (if stmt then I else PureThy.name_thms false name);
+    val thms = flat res;
   in ((bname, thms), ctxt' |> update_thms stmt (bname, SOME thms)) end);
 
 in