src/CCL/Type.thy
changeset 39159 0dec18004e75
parent 35409 5c5bb83f2bae
child 41526 54b4686704af
     1.1 --- a/src/CCL/Type.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/CCL/Type.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4    unfolding simp_type_defs by blast+
     1.5  
     1.6  ML {*
     1.7 -bind_thms ("case_rls", XH_to_Es (thms "XHs"));
     1.8 +bind_thms ("case_rls", XH_to_Es @{thms XHs});
     1.9  *}
    1.10  
    1.11  
    1.12 @@ -260,7 +260,7 @@
    1.13  
    1.14  lemmas iXHs = NatXH ListXH
    1.15  
    1.16 -ML {* bind_thms ("icase_rls", XH_to_Es (thms "iXHs")) *}
    1.17 +ML {* bind_thms ("icase_rls", XH_to_Es @{thms iXHs}) *}
    1.18  
    1.19  
    1.20  subsection {* Type Rules *}