src/HOL/TPTP/TPTP_Proof_Reconstruction.thy

  This ought to be sufficient for emulating extcnf_combined,
  but note that the complexity of the problem can be enormous.*)
 fun inst_parametermatch_tac ctxt thms i = fn st =>
   let
     val gls =
-      prop_of st
+      Thm.prop_of st
       |> Logic.strip_horn
       |> fst
 
     val parameters =
       if null gls then []

   match variables having identical names. Logically, this is
   a hack. But it reduces the complexity of the problem.*)
 fun nominal_inst_parametermatch_tac ctxt thm i = fn st =>
   let
     val gls =
-      prop_of st
+      Thm.prop_of st
       |> Logic.strip_horn
       |> fst
 
     val parameters =
       if null gls then []

   the hypothesis' quantifiers to have the ones appearing in the
   conclusion first.*)
 fun canonicalise_qtfr_order ctxt i = fn st =>
   let
     val gls =
-      prop_of st
+      Thm.prop_of st
       |> Logic.strip_horn
       |> fst
   in
     if null gls then raise NO_GOALS
     else

 fun forall_neg_tac candidate_consts ctxt i = fn st =>
   let
     val thy = Proof_Context.theory_of ctxt
 
     val gls =
-      prop_of st
+      Thm.prop_of st
       |> Logic.strip_horn
       |> fst
 
     val parameters =
       if null gls then ""

 fun absorb_skolem_def ctxt prob_name_opt i = fn st =>
   let
     val thy = Proof_Context.theory_of ctxt
 
     val gls =
-      prop_of st
+      Thm.prop_of st
       |> Logic.strip_horn
       |> fst
 
     val conclusion =
       if null gls then

 fun find_skolem_term ctxt consts_candidate arity = fn st =>
   let
     val _ = @{assert} (arity > 0)
 
     val gls =
-      prop_of st
+      Thm.prop_of st
       |> Logic.strip_horn
       |> fst
 
     (*extract the conclusion of each subgoal*)
     val conclusions =

 fun instantiate_skols ctxt consts_candidates i = fn st =>
   let
     val thy = Proof_Context.theory_of ctxt
 
     val gls =
-      prop_of st
+      Thm.prop_of st
       |> Logic.strip_horn
       |> fst
 
     val (params, conclusion) =
       if null gls then

 
     (*prefix a skolem term with bindings for the parameters*)
     (* val contextualise = fold absdummy (map snd params) *)
     val contextualise = fold absfree params
 
-    val skolem_cts = map (contextualise #> cterm_of thy) skolem_terms
+    val skolem_cts = map (contextualise #> Thm.cterm_of thy) skolem_terms
 
 
 (*now the instantiation code*)
 
     (*there should only be one Var -- that is from the previous application of drule leo2_skolemise. We look for it at the head position in some equation at a conclusion of a subgoal.*)

           |> maps (switch Term.add_vars [])
 
         fun make_var pre_var =
           the_single pre_var
           |> Var
-          |> cterm_of thy
+          |> Thm.cterm_of thy
           |> SOME
       in
         if null pre_var then NONE
         else make_var pre_var
      end

     * Assumes that there is a single hypothesis
 *)
 fun find_dec_arity i = fn st =>
   let
     val gls =
-      prop_of st
+      Thm.prop_of st
       |> Logic.strip_horn
       |> fst
   in
     if null gls then raise NO_GOALS
     else

 
 (*given an inference, it returns the parameters (i.e., we've already matched the leading & shared quantification in the hypothesis & conclusion clauses), and the "raw" inference*)
 fun breakdown_inference i = fn st =>
   let
     val gls =
-      prop_of st
+      Thm.prop_of st
       |> Logic.strip_horn
       |> fst
   in
     if null gls then raise NO_GOALS
     else

 fun extuni_dec_elim_rule ctxt arity i = fn st =>
   let
     val rule = extuni_dec_n ctxt arity
 
     val rule_hyp =
-      prop_of rule
+      Thm.prop_of rule
       |> Logic.dest_implies
       |> fst (*assuming that rule has single hypothesis*)
 
     (*having run break_hypothesis earlier, we know that the hypothesis
       now consists of a single literal. We can (and should)

   or implications; the number of antecedents; and the polarity
   of the original clause -- I think this will always be "false".*)
 fun standard_cnf_type ctxt i : thm -> (TPTP_Reconstruct.formula_kind * int * bool) option = fn st =>
   let
     val gls =
-      prop_of st
+      Thm.prop_of st
       |> Logic.strip_horn
       |> fst
 
     val hypos =
       if null gls then raise NO_GOALS

 
 (*difference in constants between the hypothesis clause and the conclusion clause*)
 fun clause_consts_diff thm =
   let
     val t =
-      prop_of thm
+      Thm.prop_of thm
       |> Logic.dest_implies
       |> fst
 
       (*This bit should not be needed, since Leo2 inferences don't have parameters*)
       |> TPTP_Reconstruct.strip_top_all_vars []

 (*remove quantification in hypothesis clause (! X. t), if
   X not free in t*)
 fun remove_redundant_quantification ctxt i = fn st =>
   let
     val gls =
-      prop_of st
+      Thm.prop_of st
       |> Logic.strip_horn
       |> fst
   in
     if null gls then raise NO_GOALS
     else

 (*remove quantification in the literal "(! X. t) = True/False"
   in the singleton hypothesis clause, if X not free in t*)
 fun remove_redundant_quantification_in_lit ctxt i = fn st =>
   let
     val gls =
-      prop_of st
+      Thm.prop_of st
       |> Logic.strip_horn
       |> fst
   in
     if null gls then raise NO_GOALS
     else

   in
     TPTP_Reconstruct.inference_at_node
      thy
      prob_name (#meta pannot) n
       |> the
-      |> (fn {inference_fmla, ...} => cterm_of thy inference_fmla)
+      |> (fn {inference_fmla, ...} => Thm.cterm_of thy inference_fmla)
       |> oracle_iinterp
   end
 *}