src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 30364 577edc39b501
parent 29635 31d14e9fa0da
child 30723 a3adc9a96a16
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -543,8 +543,8 @@
     1.4          fun setids t = issue_pgip (Setids {idtables = [t]})
     1.5  
     1.6          (* fake one-level nested "subtheories" by picking apart names. *)
     1.7 -        val immed_thms_of_thy = filter_out NameSpace.is_qualified o thms_of_thy
     1.8 -        fun thy_prefix s = case space_explode NameSpace.separator s of
     1.9 +        val immed_thms_of_thy = filter_out Long_Name.is_qualified o thms_of_thy
    1.10 +        fun thy_prefix s = case Long_Name.explode s of
    1.11                                      x::_::_ => SOME x  (* String.find? *)
    1.12                                    | _ => NONE
    1.13          fun subthys_of_thy s =
    1.14 @@ -553,7 +553,7 @@
    1.15          fun subthms_of_thy thy =
    1.16              (case thy_prefix thy of
    1.17                   NONE => immed_thms_of_thy thy
    1.18 -               | SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy))
    1.19 +               | SOME prf => filter (String.isPrefix (unprefix (prf ^ Long_Name.separator) thy))
    1.20                                      (thms_of_thy prf))
    1.21      in
    1.22          case (thyname,objtype) of
    1.23 @@ -642,7 +642,7 @@
    1.24          val topthy = Toplevel.theory_of o Isar.state
    1.25  
    1.26          fun splitthy id =
    1.27 -            let val comps = NameSpace.explode id
    1.28 +            let val comps = Long_Name.explode id
    1.29              in case comps of
    1.30                     (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
    1.31                   | [plainid] => (topthy(),plainid)