approximation_oracle: actually match true/false in ML, not arbitrary values;

--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Aug 25 18:36:22 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Aug 25 18:38:49 2010 +0200
@@ -3212,8 +3212,8 @@
 
   fun bad t = error ("Bad term: " ^ Syntax.string_of_term_global thy t);
 
-  fun term_of_bool True = @{term True}
-    | term_of_bool False = @{term False};
+  fun term_of_bool true = @{term True}
+    | term_of_bool false = @{term False};
 
   fun term_of_float (@{code Float} (k, l)) =
     @{term Float} $ HOLogic.mk_number @{typ int} k $ HOLogic.mk_number @{typ int} l;