--- 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])