src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML

   | is_rec_def (@{const Pure.imp} $ _ $ t2) = is_rec_def t2
   | is_rec_def (Const (@{const_name Pure.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
   | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
   | is_rec_def _ = false
 
-fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
+fun is_assum assms th = exists (fn ct => Thm.prop_of th aconv Thm.term_of ct) assms
 fun is_chained chained = member Thm.eq_thm_prop chained
 
 fun scope_of_thm global assms chained th =
   if is_chained chained th then Chained
   else if global then Global

 
 fun status_of_thm css name th =
   if Termtab.is_empty css then
     General
   else
-    let val t = prop_of th in
+    let val t = Thm.prop_of th in
       (* FIXME: use structured name *)
       if String.isSubstring ".induct" name andalso may_be_induction t then
         Induction
       else
         let val t = normalize_vars t in

 
 val sep_that = Long_Name.separator ^ Obtain.thatN
 val skolem_thesis = Name.skolem Auto_Bind.thesisN
 
 fun is_that_fact th =
-  exists_subterm (fn Free (s, _) => s = skolem_thesis | _ => false) (prop_of th)
+  exists_subterm (fn Free (s, _) => s = skolem_thesis | _ => false) (Thm.prop_of th)
   andalso String.isSuffix sep_that (Thm.get_name_hint th)
 
 datatype interest = Deal_Breaker | Interesting | Boring
 
 fun combine_interests Deal_Breaker _ = Deal_Breaker

         interest_of_prop Ts (t $ eta_expand Ts u 1)
       | interest_of_prop _ (Const (@{const_name Pure.eq}, _) $ t $ u) =
         combine_interests (interest_of_bool t) (interest_of_bool u)
       | interest_of_prop _ _ = Deal_Breaker
 
-    val t = prop_of th
+    val t = Thm.prop_of th
   in
     (interest_of_prop [] t <> Interesting andalso not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
     is_that_fact th
   end
 

       end)
     (Term.add_vars t [] |> sort_wrt (fst o fst))
   |> fst
 
 fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
-fun backquote_thm ctxt = backquote_term ctxt o prop_of
+fun backquote_thm ctxt = backquote_term ctxt o Thm.prop_of
 
 (* TODO: rewrite to use nets and/or to reuse existing data structures *)
 fun clasimpset_rule_table_of ctxt =
   let val simps = ctxt |> simpset_of |> dest_ss |> #simps in
     if length simps >= max_simps_for_clasimpset then
       Termtab.empty
     else
       let
-        fun add stature th = Termtab.update (normalize_vars (prop_of th), stature)
+        fun add stature th = Termtab.update (normalize_vars (Thm.prop_of th), stature)
 
         val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} = ctxt |> claset_of |> Classical.rep_cs
         val intros = Item_Net.content safeIs @ Item_Net.content hazIs
 (* Add once it is used:
         val elims = Item_Net.content safeEs @ Item_Net.content hazEs

         val specs = Spec_Rules.get ctxt
         val (rec_defs, nonrec_defs) = specs
           |> filter (curry (op =) Spec_Rules.Equational o fst)
           |> maps (snd o snd)
           |> filter_out (member Thm.eq_thm_prop risky_defs)
-          |> List.partition (is_rec_def o prop_of)
+          |> List.partition (is_rec_def o Thm.prop_of)
         val spec_intros = specs
           |> filter (member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] o fst)
           |> maps (snd o snd)
       in
         Termtab.empty

     SOME (pref, suf) => [s, pref ^ suf]
   | NONE => [s])
 
 fun build_name_tables name_of facts =
   let
-    fun cons_thm (_, th) = Termtab.cons_list (normalize_vars (normalize_eq (prop_of th)), th)
+    fun cons_thm (_, th) = Termtab.cons_list (normalize_vars (normalize_eq (Thm.prop_of th)), th)
     fun add_plain canon alias =
       Symtab.update (Thm.get_name_hint alias, name_of (if_thm_before canon alias))
     fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
     fun add_inclass (name, target) = fold (fn s => Symtab.update (s, target)) (un_class_ify name)
     val prop_tab = fold cons_thm facts Termtab.empty

     (plain_name_tab, inclass_name_tab)
   end
 
 fun fact_distinct eq facts =
   fold (fn fact as (_, th) =>
-      Net.insert_term_safe (eq o apply2 (normalize_eq o prop_of o snd))
-        (normalize_eq (prop_of th), fact))
+      Net.insert_term_safe (eq o apply2 (normalize_eq o Thm.prop_of o snd))
+        (normalize_eq (Thm.prop_of th), fact))
     facts Net.empty
   |> Net.entries
 
 fun struct_induct_rule_on th =
-  (case Logic.strip_horn (prop_of th) of
+  (case Logic.strip_horn (Thm.prop_of th) of
     (prems, @{const Trueprop} $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
     if not (is_TVar ind_T) andalso length prems > 1 andalso
        exists (exists_subterm (curry (op aconv) p)) prems andalso
        not (exists (exists_subterm (curry (op aconv) a)) prems) then
       SOME (p_name, ind_T)

           in
             snd (fold_rev (fn th => fn (j, accum) =>
               (j - 1,
                if not (member Thm.eq_thm_prop add_ths th) andalso
                   (is_likely_tautology_too_meta_or_too_technical th orelse
-                   is_too_complex (prop_of th)) then
+                   is_too_complex (Thm.prop_of th)) then
                  accum
                else
                  let
                    fun get_name () =
                      if name0 = "" then