src/HOL/Tools/float_arith.ML
changeset 37391 476270a6c2dc
parent 29804 e15b74577368
     1.1 --- a/src/HOL/Tools/float_arith.ML	Thu Jun 10 12:24:02 2010 +0200
     1.2 +++ b/src/HOL/Tools/float_arith.ML	Thu Jun 10 12:24:03 2010 +0200
     1.3 @@ -206,7 +206,7 @@
     1.4  fun mk_float (a, b) = @{term "float"} $
     1.5    HOLogic.mk_prod (pairself (HOLogic.mk_number HOLogic.intT) (a, b));
     1.6  
     1.7 -fun dest_float (Const ("Float.float", _) $ (Const ("Pair", _) $ a $ b)) =
     1.8 +fun dest_float (Const ("Float.float", _) $ (Const (@{const_name Pair}, _) $ a $ b)) =
     1.9        pairself (snd o HOLogic.dest_number) (a, b)
    1.10    | dest_float t = ((snd o HOLogic.dest_number) t, 0);
    1.11