diff -r 9963bb965a0e -r 4bc4b5c0ccfc src/HOL/Nonstandard_Analysis/HTranscendental.thy
--- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Tue Jul 10 09:52:22 2018 +0100
+++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Tue Jul 10 23:18:08 2018 +0100
@@ -60,7 +60,7 @@
     "!!x y. [|0 < x; 0 <y |] ==>
       ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
 apply transfer
-apply (auto intro: real_sqrt_mult_distrib) 
+apply (auto intro: real_sqrt_mult) 
 done
 
 lemma hypreal_sqrt_mult_distrib2: