diff -r 09ee87ef8b43 -r 84f20233d466 src/HOL/Matrix/Compute_Oracle/am.ML
--- a/src/HOL/Matrix/Compute_Oracle/am.ML	Fri Feb 10 23:16:24 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am.ML	Fri Feb 10 23:23:41 2012 +0100
@@ -15,8 +15,6 @@
    1 to the second last, and so on. *)
 val compile : (guard list * pattern * term) list -> program
 
-val discard : program -> unit
-
 exception Run of string;
 val run : program -> term -> term
 
@@ -66,8 +64,6 @@
 
 fun compile _ = raise Compile "abstract machine stub"
 
-fun discard _ = raise Compile "abstract machine stub"
-
 exception Run of string;
 
 fun run _ _ = raise Run "abstract machine stub"