changeset 46711 | f745bcc4a1e5 |
parent 45666 | d83797ef0d2d |
child 46829 | 9770573e2172 |
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Feb 27 16:53:13 2012 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Feb 27 16:56:25 2012 +0100 @@ -642,7 +642,7 @@ fun splitthy id = let val comps = Long_Name.explode id in case comps of - (thy::(rest as _::_)) => (Thy_Info.get_theory thy, space_implode "." rest) + (thy::(rest as _::_)) => (Thy_Info.get_theory thy, Long_Name.implode rest) | [plainid] => (topthy(),plainid) | _ => raise Toplevel.UNDEF (* assert false *) end