1.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Mon Nov 23 19:03:16 2009 +0100
     1.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Mon Nov 23 19:42:52 2009 +0100
     1.3 @@ -185,7 +185,7 @@
     1.4      by (auto simp add: rtranclp_eq_rtrancl_path)
     1.5  qed
     1.6  
     1.7 -declare rtranclp_eq_rtrancl_tab_nil [code_unfold]
     1.8 +declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del]
     1.9  
    1.10  declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
    1.11  
    1.12 @@ -224,7 +224,11 @@
    1.13  values "{x. test\<^sup>*\<^sup>* A x}"
    1.14  values "{x. test\<^sup>*\<^sup>* x C}"
    1.15  
    1.16 -hide const test
    1.17 +value "test\<^sup>*\<^sup>* A C"
    1.18 +value "test\<^sup>*\<^sup>* C A"
    1.19 +
    1.20 +hide type ty
    1.21 +hide const test A B C
    1.22  
    1.23  end
    1.24