src/HOL/Code_Evaluation.thy
changeset 36176 3fe7e97ccca8
parent 35845 e5980f0ad025
child 38348 cf7b2121ad9d
     1.1 --- a/src/HOL/Code_Evaluation.thy	Fri Apr 16 20:56:40 2010 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Fri Apr 16 21:28:09 2010 +0200
     1.3 @@ -280,8 +280,8 @@
     1.4  end
     1.5  *}
     1.6  
     1.7 -hide const dummy_term App valapp
     1.8 -hide (open) const Const termify valtermify term_of term_of_num
     1.9 +hide_const dummy_term App valapp
    1.10 +hide_const (open) Const termify valtermify term_of term_of_num
    1.11  
    1.12  subsection {* Tracing of generated and evaluated code *}
    1.13  
    1.14 @@ -301,7 +301,7 @@
    1.15  code_const "tracing :: String.literal => 'a => 'a"
    1.16    (Eval "Code'_Evaluation.tracing")
    1.17  
    1.18 -hide (open) const tracing
    1.19 +hide_const (open) tracing
    1.20  code_reserved Eval Code_Evaluation
    1.21  
    1.22  subsection {* Evaluation setup *}