src/HOL/Matrix/Compute_Oracle/am_interpreter.ML

--- a/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML	Fri Feb 10 23:16:24 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML	Fri Feb 10 23:23:41 2012 +0100
@@ -208,6 +208,4 @@
            | _ => raise (Run "internal error in run: weak failed")
      end handle InterruptedExecution state => term_of_clos (resolve state))
 
-fun discard _ = ()
-
 end