src/CCL/Term.thy
changeset 56199 8e8d28ed7529
parent 52143 36ffe23b25f8
child 58889 5b7a9633cfa8
     1.1 --- a/src/CCL/Term.thy	Tue Mar 18 10:00:23 2014 +0100
     1.2 +++ b/src/CCL/Term.thy	Tue Mar 18 11:07:47 2014 +0100
     1.3 @@ -286,7 +286,7 @@
     1.4  subsection {* Constructors are distinct *}
     1.5  
     1.6  ML {*
     1.7 -bind_thms ("term_dstncts",
     1.8 +ML_Thms.bind_thms ("term_dstncts",
     1.9    mkall_dstnct_thms @{context} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs})
    1.10      [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
    1.11  *}
    1.12 @@ -305,7 +305,7 @@
    1.13  subsection {* Rewriting and Proving *}
    1.14  
    1.15  ML {*
    1.16 -  bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
    1.17 +  ML_Thms.bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
    1.18  *}
    1.19  
    1.20  lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews