src/HOL/Library/Extended_Nat.thy
changeset 59582 0fbed69ff081
parent 59115 f65ac77f7e07
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -561,15 +561,15 @@
     1.4  
     1.5  simproc_setup enat_eq_cancel
     1.6    ("(l::enat) + m = n" | "(l::enat) = m + n") =
     1.7 -  {* fn phi => fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (term_of ct) *}
     1.8 +  {* fn phi => fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct) *}
     1.9  
    1.10  simproc_setup enat_le_cancel
    1.11    ("(l::enat) + m \<le> n" | "(l::enat) \<le> m + n") =
    1.12 -  {* fn phi => fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (term_of ct) *}
    1.13 +  {* fn phi => fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct) *}
    1.14  
    1.15  simproc_setup enat_less_cancel
    1.16    ("(l::enat) + m < n" | "(l::enat) < m + n") =
    1.17 -  {* fn phi => fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (term_of ct) *}
    1.18 +  {* fn phi => fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct) *}
    1.19  
    1.20  text {* TODO: add regression tests for these simprocs *}
    1.21