src/HOL/Orderings.thy

 local
   fun prp t thm = Thm.prop_of thm = t;  (* FIXME proper aconv!? *)
 in
 
 fun antisym_le_simproc ctxt ct =
-  (case term_of ct of
+  (case Thm.term_of ct of
     (le as Const (_, T)) $ r $ s =>
      (let
         val prems = Simplifier.prems_of ctxt;
         val less = Const (@{const_name less}, T);
         val t = HOLogic.mk_Trueprop(le $ s $ r);

          | SOME thm => SOME (mk_meta_eq (thm RS @{thm order_class.antisym_conv})))
       end handle THM _ => NONE)
   | _ => NONE);
 
 fun antisym_less_simproc ctxt ct =
-  (case term_of ct of
+  (case Thm.term_of ct of
     NotC $ ((less as Const(_,T)) $ r $ s) =>
      (let
        val prems = Simplifier.prems_of ctxt;
        val le = Const (@{const_name less_eq}, T);
        val t = HOLogic.mk_Trueprop(le $ r $ s);