diff -r 151fef652324 -r 6014e8252e57 src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Fri Oct 29 16:04:35 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Fri Oct 29 17:25:22 2010 +0200
@@ -105,7 +105,7 @@
 
 section {* Example symbolic derivation *}
 
-hide_const Plus Pow
+hide_const Pow
 
 datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
   | Minus expr expr | Uminus expr | Pow expr int | Exp expr