Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/numeral_simprocs.ML
changeset 81942 da3c3948a39c
parent 80701 39cd50407f79 
--- a/src/HOL/Tools/numeral_simprocs.ML	Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Tue Jan 21 16:22:15 2025 +0100
@@ -471,7 +471,7 @@
     simplify_one ctxt (([th, cancel_th]) MRS trans);
 
 local
-  val Tp_Eq = Thm.reflexive (Thm.cterm_of \<^theory_context>\<open>HOL\<close> HOLogic.Trueprop)
+  val Tp_Eq = Thm.reflexive \<^cterm>\<open>Trueprop\<close>
   fun Eq_True_elim Eq =
     Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
 in
@@ -593,7 +593,7 @@
     val eq = Thm.instantiate_cterm (TVars.make1 (type_tvar, T), Vars.empty) geq
     val th =
       Simplifier.rewrite (ctxt addsimps @{thms simp_thms})
-        (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply \<^cterm>\<open>Not\<close>
+        (HOLogic.mk_judgment (Thm.apply \<^cterm>\<open>Not\<close>
           (Thm.apply (Thm.apply eq t) z)))
   in Thm.equal_elim (Thm.symmetric th) TrueI end
isabelle