dropped obsolete Theory.sign_of
authorhaftmann
Mon, 02 Oct 2006 23:00:52 +0200
changeset 20836 9e40d815e002
parent 20835 27d049062b56
child 20837 099877d83d2b
dropped obsolete Theory.sign_of
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