lists.ml.patch

509,514d508
< let BUTLAST_CLAUSES = prove
<  (`BUTLAST([]:A list) = [] /\
<    (!a:A. BUTLAST [a] = []) /\
<    (!(a:A) h t. BUTLAST(CONS a (CONS h t)) = CONS a (BUTLAST(CONS h t)))`,
<   REWRITE_TAC[BUTLAST; NOT_CONS_NIL]);;
< 
733,734c727,728
<         let ccs = map (String.make 1 o char_of_term) tms in
<         String.escaped (implode ccs)
---
>         let ccs = map (String.str o char_of_term) tms in
>         string_escaped (implode ccs)
744,746c738,740
<     let codes = Array.map mk_code (Array.of_list (0--255)) in
<     fun c -> Array.get codes c in
<   let mk_char = mk_code o Char.code in
---
>     let codes = Array.fromList (List.map mk_code (0--255)) in
>     fun c -> Array.sub codes c in
>   let mk_char = mk_code o Char.ord in
748,749c742,743
<     let ns = map (fun i -> Char.code(String.get s i))
<                  (0--(String.length s - 1)) in
---
>     let ns = map (fun i -> Char.ord(String.sub s i))
>                  (0--(String.size s - 1)) in
818c812
<   let CHAR_EQ_CONV : conv =
---
>   let (CHAR_EQ_CONV : conv) =
821c815
<       if compare c1 c2 = 0 then EQT_INTRO (REFL c1) else
---
>       if c1 = c2 then EQT_INTRO (REFL c1) else
825c819
<     if compare ltm rtm = 0 then EQT_INTRO (REFL ltm) else
---
>     if ltm = rtm then EQT_INTRO (REFL ltm) else