src/HOL/Tools/Qelim/cooper.ML

          |> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end
   fun nzprop x =
    let
     val th =
      Simplifier.rewrite (put_simpset lin_ss ctxt)
-      (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 \<^cterm>\<open>(=) :: int => _\<close> (Numeral.mk_cnumber \<^ctyp>\<open>int\<close> x))
            \<^cterm>\<open>0::int\<close>)))
    in Thm.equal_elim (Thm.symmetric th) TrueI end;
   val notz =
     let val tab = fold Inttab.update

  val cd = Numeral.mk_cnumber \<^ctyp>\<open>int\<close> d
  fun divprop x =
    let
     val th =
      Simplifier.rewrite (put_simpset lin_ss ctxt)
-      (Thm.apply \<^cterm>\<open>Trueprop\<close>
+      (HOLogic.mk_judgment
            (Thm.apply (Thm.apply dvdc (Numeral.mk_cnumber \<^ctyp>\<open>int\<close> x)) cd))
    in Thm.equal_elim (Thm.symmetric th) TrueI end;
  val dvd =
    let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
      fn ct => the (Inttab.lookup tab (Thm.term_of ct |> dest_number))

         (writeln ("dvd: Theorems-Table contains no entry for" ^
             Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option.Option)
    end
  val dp =
    let val th = Simplifier.rewrite (put_simpset lin_ss ctxt)
-      (Thm.apply \<^cterm>\<open>Trueprop\<close>
+      (HOLogic.mk_judgment
            (Thm.apply (Thm.apply \<^cterm>\<open>(<) :: int => _\<close> \<^cterm>\<open>0::int\<close>) cd))
    in Thm.equal_elim (Thm.symmetric th) TrueI end;
     (* A and B set *)
    local
      val insI1 = Thm.instantiate' [SOME \<^ctyp>\<open>int\<close>] [] @{thm "insertI1"}

      val (ps, c) = split_last (strip_objimp p)
      val qs = filter P ps
      val q = if P c then c else \<^cterm>\<open>False\<close>
      val ng = fold_rev (fn (a,v) => fn t => Thm.apply a (Thm.lambda v t)) qvs
          (fold_rev (fn p => fn q => Thm.apply (Thm.apply \<^cterm>\<open>HOL.implies\<close> p) q) qs q)
-     val g = Thm.apply (Thm.apply \<^cterm>\<open>(==>)\<close> (Thm.apply \<^cterm>\<open>Trueprop\<close> ng)) p'
+     val g = Thm.apply (Thm.apply \<^cterm>\<open>(==>)\<close> (HOLogic.mk_judgment ng)) p'
      val ntac = (case qs of [] => q aconvc \<^cterm>\<open>False\<close>
                          | _ => false)
     in
       if ntac then no_tac
       else