diff -r 056255ade52a -r 4e74209f113e src/HOL/NSA/HLog.thy
--- a/src/HOL/NSA/HLog.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HLog.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -20,11 +20,11 @@
 
 definition
   powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80) where
-  [transfer_unfold, code func del]: "x powhr a = starfun2 (op powr) x a"
+  [transfer_unfold, code del]: "x powhr a = starfun2 (op powr) x a"
   
 definition
   hlog :: "[hypreal,hypreal] => hypreal" where
-  [transfer_unfold, code func del]: "hlog a x = starfun2 log a x"
+  [transfer_unfold, code del]: "hlog a x = starfun2 log a x"
 
 lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
 by (simp add: powhr_def starfun2_star_n)