diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Aug 19 16:08:59 2010 +0200
@@ -3301,10 +3301,10 @@
 ML {*
   fun reorder_bounds_tac prems i =
     let
-      fun variable_of_bound (Const (@{const_name "Trueprop"}, _) $
+      fun variable_of_bound (Const (@{const_name Trueprop}, _) $
                              (Const (@{const_name Set.member}, _) $
                               Free (name, _) $ _)) = name
-        | variable_of_bound (Const (@{const_name "Trueprop"}, _) $
+        | variable_of_bound (Const (@{const_name Trueprop}, _) $
                              (Const (@{const_name "op ="}, _) $
                               Free (name, _) $ _)) = name
         | variable_of_bound t = raise TERM ("variable_of_bound", [t])