src/Pure/Proof/extraction.ML
changeset 40627 becf5d5187cc
parent 40132 7ee65dbffa31
child 40844 5895c525739d
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4    | rlz_proc _ = NONE;
     1.5  
     1.6  val unpack_ixn = apfst implode o apsnd (fst o read_int o tl) o
     1.7 -  take_prefix (fn s => s <> ":") o explode;
     1.8 +  take_prefix (fn s => s <> ":") o raw_explode;
     1.9  
    1.10  type rules =
    1.11    {next: int, rs: ((term * term) list * (term * term)) list,