1.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Feb 27 16:53:13 2012 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Feb 27 16:56:25 2012 +0100
     1.3 @@ -360,7 +360,7 @@
     1.4     constant name. *)
     1.5  fun num_type_args thy s =
     1.6    if String.isPrefix skolem_const_prefix s then
     1.7 -    s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
     1.8 +    s |> Long_Name.explode |> List.last |> Int.fromString |> the
     1.9    else if String.isPrefix lam_lifted_prefix s then
    1.10      if String.isPrefix lam_lifted_poly_prefix s then 2 else 0
    1.11    else