diff -r faf233c4a404 -r 55fea563fbee src/HOL/Matrix/Compute_Oracle/am.ML
--- 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