# HG changeset patch
# User haftmann
# Date 1159822852 -7200
# Node ID 9e40d815e00201cf317fb485647c020c6f375367
# Parent  27d049062b560f2fc5e85459c5bdd2ab63d290ef
dropped obsolete Theory.sign_of

diff -r 27d049062b56 -r 9e40d815e002 src/HOL/antisym_setup.ML
--- a/src/HOL/antisym_setup.ML	Mon Oct 02 23:00:51 2006 +0200
+++ b/src/HOL/antisym_setup.ML	Mon Oct 02 23:00:52 2006 +0200
@@ -40,9 +40,9 @@
   end
   handle THM _ => NONE;
 
-val antisym_le = Simplifier.simproc (Theory.sign_of (the_context()))
+val antisym_le = Simplifier.simproc (the_context())
   "antisym le" ["(x::'a::order) <= y"] prove_antisym_le;
-val antisym_less = Simplifier.simproc (Theory.sign_of (the_context()))
+val antisym_less = Simplifier.simproc (the_context())
   "antisym less" ["~ (x::'a::linorder) < y"] prove_antisym_less;
 
 in