src/HOL/Orderings.thy

--- a/src/HOL/Orderings.thy	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Orderings.thy	Wed Mar 04 19:53:18 2015 +0100
@@ -608,7 +608,7 @@
 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;
@@ -627,7 +627,7 @@
   | _ => 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;