src/HOL/Product_Type.thy

   this rule directly --- it loops!
 *}
 
 simproc_setup unit_eq ("x::unit") = {*
   fn _ => fn _ => fn ct =>
-    if HOLogic.is_unit (term_of ct) then NONE
+    if HOLogic.is_unit (Thm.term_of ct) then NONE
     else SOME (mk_meta_eq @{thm unit_eq})
 *}
 
 free_constructors case_unit for "()"
   by auto

           SOME (_, ft) => SOME (metaeq ctxt s (let val f $ _ = ft in f end))
         | NONE => NONE)
     | eta_proc _ _ = NONE;
 end;
 *}
-simproc_setup split_beta ("split f z") = {* fn _ => fn ctxt => fn ct => beta_proc ctxt (term_of ct) *}
-simproc_setup split_eta ("split f") = {* fn _ => fn ctxt => fn ct => eta_proc ctxt (term_of ct) *}
+simproc_setup split_beta ("split f z") =
+  {* fn _ => fn ctxt => fn ct => beta_proc ctxt (Thm.term_of ct) *}
+simproc_setup split_eta ("split f") =
+  {* fn _ => fn ctxt => fn ct => eta_proc ctxt (Thm.term_of ct) *}
 
 lemmas split_beta [mono] = prod.case_eq_if
 
 lemma split_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
   by (auto simp: fun_eq_iff)

 subsection {* Inductively defined sets *}
 
 (* simplify {(x1, ..., xn). (x1, ..., xn) : S} to S *)
 simproc_setup Collect_mem ("Collect t") = {*
   fn _ => fn ctxt => fn ct =>
-    (case term_of ct of
+    (case Thm.term_of ct of
       S as Const (@{const_name Collect}, Type (@{type_name fun}, [_, T])) $ t =>
         let val (u, _, ps) = HOLogic.strip_psplits t in
           (case u of
             (c as Const (@{const_name Set.member}, _)) $ q $ S' =>
               (case try (HOLogic.strip_ptuple ps) q of