src/Pure/Proof/extraction.ML

        | (Free (s, U), ts) => SOME (list_comb (Free (s, T --> U), r :: ts))
        | _ => NONE)
   | rlz_proc _ = NONE;
 
 val unpack_ixn = apfst implode o apsnd (fst o read_int o tl) o
-  take_prefix (fn s => s <> ":") o explode;
+  take_prefix (fn s => s <> ":") o raw_explode;
 
 type rules =
   {next: int, rs: ((term * term) list * (term * term)) list,
    net: (int * ((term * term) list * (term * term))) Net.net};