# HG changeset patch
# User wenzelm
# Date 1121362095 -7200
# Node ID a4e99217e9f9722a7a54ede6f44eb23004e825d2
# Parent  f220d1df0f4e68780a50aafeea7925a02d906274
HOL.Not;

diff -r f220d1df0f4e -r a4e99217e9f9 src/HOL/antisym_setup.ML
--- a/src/HOL/antisym_setup.ML	Thu Jul 14 19:28:14 2005 +0200
+++ b/src/HOL/antisym_setup.ML	Thu Jul 14 19:28:15 2005 +0200
@@ -1,3 +1,6 @@
+
+(* $Id$ *)
+
 local
 
 val order_antisym_conv = thm "order_antisym_conv"
@@ -13,7 +16,7 @@
       val t = HOLogic.mk_Trueprop(le $ s $ r);
   in case Library.find_first (prp t) prems of
        NONE =>
-         let val t = HOLogic.mk_Trueprop(HOLogic.not_const $ (less $ r $ s))
+         let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s))
          in case Library.find_first (prp t) prems of
               NONE => NONE
             | SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv1))
@@ -47,4 +50,4 @@
 val antisym_setup =
  [Simplifier.change_simpset_of (op addsimprocs) [antisym_le,antisym_less]];
 
-end
\ No newline at end of file
+end