# HG changeset patch
# User wenzelm
# Date 1213281720 -7200
# Node ID adefd34541741914804aa148893be971f7ebadc9
# Parent  3735b80d06fcf6bcc893e2b382f098fad12810ab
sane versions of (qualified_)thms_of_thy;

diff -r 3735b80d06fc -r adefd3454174 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Jun 12 16:41:58 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Jun 12 16:42:00 2008 +0200
@@ -563,6 +563,18 @@
 fun addids t  = issue_pgip (Addids {idtables = [t]})
 fun delids t  = issue_pgip (Delids {idtables = [t]})
 
+
+local
+
+fun theory_facts name =
+  let val thy = ThyInfo.get_theory name
+  in (map PureThy.facts_of (Theory.parents_of thy), PureThy.facts_of thy) end;
+
+fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static);
+fun qualified_thms_of_thy name = map fst (theory_facts name |-> Facts.dest_static);
+
+in
+
 fun askids (Askids vs) =
     let
         val url = #url vs            (* ask for identifiers within a file *)
@@ -574,8 +586,6 @@
         fun setids t = issue_pgip (Setids {idtables = [t]})
 
         (* fake one-level nested "subtheories" by picking apart names. *)
-        val thms_of_thy =
-            map fst o NameSpace.extern_table o PureThy.theorems_of o ThyInfo.get_theory
         val immed_thms_of_thy = filter_out NameSpace.is_qualified o thms_of_thy
         fun thy_prefix s = case space_explode NameSpace.separator s of
                                     x::_::_ => SOME x  (* String.find? *)
@@ -588,13 +598,6 @@
                  NONE => immed_thms_of_thy thy
                | SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy))
                                     (thms_of_thy prf))
-       val qualified_thms_of_thy = (* for global query with single response *)
-            (map fst) o NameSpace.dest_table o PureThy.theorems_of o ThyInfo.get_theory;
-(* da: this version is equivalent to my previous, but splits up theorem sets with names
-   that I can't get to access later with get_thm.  Anyway, would rather use sets.
-   Is above right way to get qualified names in that case?  Filtering required again?
-            map PureThy.get_name_hint o filter PureThy.has_name_hint o
-              map snd o PureThy.thms_of o ThyInfo.get_theory; *)
     in
         case (thyname,objtype) of
            (NONE, NONE) =>
@@ -619,6 +622,8 @@
          | _ => warning ("askids: ignored argument combination")
     end
 
+end;
+
 fun askrefs (Askrefs vs) =
     let
         val url = #url vs            (* ask for references of a file (i.e. immediate pre-requisites) *)