--- a/src/HOL/Matrix/Compute_Oracle/am.ML Fri Feb 10 23:06:21 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am.ML Fri Feb 10 23:12:57 2012 +0100
@@ -13,7 +13,7 @@
(* The de-Bruijn index 0 occurring on the right hand side refers to the LAST pattern variable, when traversing the pattern from left to right,
1 to the second last, and so on. *)
-val compile : pattern list -> (int -> int option) -> (guard list * pattern * term) list -> program
+val compile : (guard list * pattern * term) list -> program
val discard : program -> unit