src/HOL/Orderings.thy
changeset 59582 0fbed69ff081
parent 59000 6eb0725503fc
child 59936 b8ffc3dc9e24
     1.1 --- a/src/HOL/Orderings.thy	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -608,7 +608,7 @@
     1.4  in
     1.5  
     1.6  fun antisym_le_simproc ctxt ct =
     1.7 -  (case term_of ct of
     1.8 +  (case Thm.term_of ct of
     1.9      (le as Const (_, T)) $ r $ s =>
    1.10       (let
    1.11          val prems = Simplifier.prems_of ctxt;
    1.12 @@ -627,7 +627,7 @@
    1.13    | _ => NONE);
    1.14  
    1.15  fun antisym_less_simproc ctxt ct =
    1.16 -  (case term_of ct of
    1.17 +  (case Thm.term_of ct of
    1.18      NotC $ ((less as Const(_,T)) $ r $ s) =>
    1.19       (let
    1.20         val prems = Simplifier.prems_of ctxt;