src/HOL/Tools/Argo/argo_tactic.ML

   | term_of (cx as (ctxt, _)) e =
       (case ext_term_of ctxt (term_of cx) e of
         SOME t => t
       | NONE => raise Fail "bad expression")
 
-fun as_prop ct = Thm.apply \<^cterm>\<open>Trueprop\<close> ct
-
 fun cterm_of ctxt cons e = Thm.cterm_of ctxt (term_of (ctxt, cons) e)
-fun cprop_of ctxt cons e = as_prop (cterm_of ctxt cons e)
+fun cprop_of ctxt cons e = HOLogic.mk_judgment (cterm_of ctxt cons e)
 
 
 (* generic proof tools *)
 
 fun discharge thm rule = thm INCR_COMP rule
 fun discharge2 thm1 thm2 rule = discharge thm2 (discharge thm1 rule)
 fun discharges thm rules = [thm] RL rules
 
 fun under_assumption f ct =
-  let val cprop = as_prop ct
+  let val cprop = HOLogic.mk_judgment ct
   in Thm.implies_intr cprop (f (Thm.assume cprop)) end
 
 
 (* proof replay for tautologies *)
 

 val dneg_rule = @{lemma "\<not>\<not>P \<Longrightarrow> P" by auto}
 
 fun replay_hyp i ct =
   if i < 0 then (Thm.assume ct, [(~i, ct)])
   else
-    let val cu = as_prop (Thm.apply \<^cterm>\<open>Not\<close> (Thm.apply \<^cterm>\<open>Not\<close> (Thm.dest_arg ct)))
+    let val cu = HOLogic.mk_judgment (Thm.apply \<^cterm>\<open>Not\<close> (Thm.apply \<^cterm>\<open>Not\<close> (Thm.dest_arg ct)))
     in (discharge (Thm.assume cu) dneg_rule, [(~i, cu)]) end
 
 
 (* proof replay for lemma *)