--- a/src/HOL/Decision_Procs/Approximation.thy Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Jun 10 12:24:03 2010 +0200
@@ -3440,7 +3440,7 @@
fun dest_float (@{const "Float"} $ m $ e) = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
fun dest_ivl (Const (@{const_name "Some"}, _) $
- (Const (@{const_name "Pair"}, _) $ u $ l)) = SOME (dest_float u, dest_float l)
+ (Const (@{const_name Pair}, _) $ u $ l)) = SOME (dest_float u, dest_float l)
| dest_ivl (Const (@{const_name "None"}, _)) = NONE
| dest_ivl t = raise TERM ("dest_result", [t])