src/HOL/Matrix_LP/float_arith.ML

     val r = signint ep (str2int e) - s
   in
     approx_dec_by_bin n (q,r)
   end
 
-fun mk_float (a, b) = @{term "float"} $
+fun mk_float (a, b) = \<^term>\<open>float\<close> $
   HOLogic.mk_prod (apply2 (HOLogic.mk_number HOLogic.intT) (a, b));
 
-fun dest_float (Const (@{const_name float}, _) $ (Const (@{const_name Pair}, _) $ a $ b)) =
+fun dest_float (Const (\<^const_name>\<open>float\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ a $ b)) =
       apply2 (snd o HOLogic.dest_number) (a, b)
   | dest_float t = ((snd o HOLogic.dest_number) t, 0);
 
 fun approx_float prec f value =
   let