src/HOL/Code_Evaluation.thy
changeset 36176 3fe7e97ccca8
parent 35845 e5980f0ad025
child 38348 cf7b2121ad9d
--- a/src/HOL/Code_Evaluation.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -280,8 +280,8 @@
 end
 *}
 
-hide const dummy_term App valapp
-hide (open) const Const termify valtermify term_of term_of_num
+hide_const dummy_term App valapp
+hide_const (open) Const termify valtermify term_of term_of_num
 
 subsection {* Tracing of generated and evaluated code *}
 
@@ -301,7 +301,7 @@
 code_const "tracing :: String.literal => 'a => 'a"
   (Eval "Code'_Evaluation.tracing")
 
-hide (open) const tracing
+hide_const (open) tracing
 code_reserved Eval Code_Evaluation
 
 subsection {* Evaluation setup *}