equal
deleted
inserted
replaced
27 |
27 |
28 fun save_result r = (saved_result := SOME r) |
28 fun save_result r = (saved_result := SOME r) |
29 fun clear_result () = (saved_result := NONE) |
29 fun clear_result () = (saved_result := NONE) |
30 |
30 |
31 val list_nth = List.nth |
31 val list_nth = List.nth |
32 |
|
33 (*fun list_nth (l,n) = (writeln (makestring ("list_nth", (length l,n))); List.nth (l,n))*) |
|
34 |
32 |
35 val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option) |
33 val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option) |
36 |
34 |
37 fun set_compiled_rewriter r = (compiled_rewriter := SOME r) |
35 fun set_compiled_rewriter r = (compiled_rewriter := SOME r) |
38 |
36 |