src/HOL/Library/Extended_Nat.thy
changeset 59582 0fbed69ff081
parent 59115 f65ac77f7e07
child 60500 903bb1495239
--- a/src/HOL/Library/Extended_Nat.thy	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Wed Mar 04 19:53:18 2015 +0100
@@ -561,15 +561,15 @@
 
 simproc_setup enat_eq_cancel
   ("(l::enat) + m = n" | "(l::enat) = m + n") =
-  {* fn phi => fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (term_of ct) *}
+  {* fn phi => fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct) *}
 
 simproc_setup enat_le_cancel
   ("(l::enat) + m \<le> n" | "(l::enat) \<le> m + n") =
-  {* fn phi => fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (term_of ct) *}
+  {* fn phi => fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct) *}
 
 simproc_setup enat_less_cancel
   ("(l::enat) + m < n" | "(l::enat) < m + n") =
-  {* fn phi => fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (term_of ct) *}
+  {* fn phi => fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct) *}
 
 text {* TODO: add regression tests for these simprocs *}