--- 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