diff -r de5cd9217d4c -r eabf80376aab src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Library/Float.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -590,7 +590,7 @@
 
 qualified lemma compute_float_sgn[code]:
   "sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)"
-  by transfer (simp add: sgn_times)
+  by transfer (simp add: sgn_mult)
 
 lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" .