equal
deleted
inserted
replaced
100 let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1); |
100 let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1); |
101 in nr 0 end; |
101 in nr 0 end; |
102 *} |
102 *} |
103 |
103 |
104 "arbitrary" ("(raise Match)") |
104 "arbitrary" ("(raise Match)") |
105 "arbitrary" :: "val" ("{* Unit *}") |
105 "arbitrary :: val" ("{* Unit *}") |
106 "arbitrary" :: "cname" ("{* Object *}") |
106 "arbitrary :: cname" ("{* Object *}") |
107 |
107 |
108 "list_nam" ("\"list\"") |
108 "list_nam" ("\"list\"") |
109 "test_nam" ("\"test\"") |
109 "test_nam" ("\"test\"") |
110 "append_name" ("\"append\"") |
110 "append_name" ("\"append\"") |
111 "makelist_name" ("\"makelist\"") |
111 "makelist_name" ("\"makelist\"") |