src/HOL/Matrix/Compute_Oracle/am_sml.ML

--- a/src/HOL/Matrix/Compute_Oracle/am_sml.ML	Fri Feb 10 23:06:21 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_sml.ML	Fri Feb 10 23:12:57 2012 +0100
@@ -490,7 +490,7 @@
 
 fun use_source src = use_text ML_Env.local_context (1, "") false src
     
-fun compile _ _ eqs = 
+fun compile eqs = 
     let
         val guid = get_guid ()
         val code = Real.toString (random ())