# HG changeset patch
# User wenzelm
# Date 1170673432 -3600
# Node ID 0f24888c8591408ed4fe1e6867354be6c0f44997
# Parent  020f65c2cdabcdc160220dc9df3b2dec40838e1c
proper use of NameSpace.is_qualified (avoids compatibility issues of the SML B library);

diff -r 020f65c2cdab -r 0f24888c8591 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Feb 04 22:02:22 2007 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Feb 05 12:03:52 2007 +0100
@@ -579,9 +579,8 @@
 
         (* 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 isnested_id =  String.isSubstring NameSpace.separator
-        val immed_thms_of_thy = filter_out isnested_id o 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? *)
                                   | _ => NONE