# HG changeset patch
# User wenzelm
# Date 1282754329 -7200
# Node ID 3c3b4ad683d59c32665f9dc521bd89172129c054
# Parent  6513ea67d95dbfde0ee44555b257076a65f4a58f
approximation_oracle: actually match true/false in ML, not arbitrary values;

diff -r 6513ea67d95d -r 3c3b4ad683d5 src/HOL/Decision_Procs/Approximation.thy
--- 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;