# HG changeset patch
# User wenzelm
# Date 1188663458 -7200
# Node ID d4dc5dc2db98e82af083b5c9668a6e301785d865
# Parent  540eaf87e42dbebb7402eee7aeb90447ad41c720
linorder_neqE_ordered_idom: proper proof, avoid illegal schematic type vars;

diff -r 540eaf87e42d -r d4dc5dc2db98 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Sat Sep 01 18:17:36 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Sat Sep 01 18:17:38 2007 +0200
@@ -347,8 +347,10 @@
 
 class ordered_field = field + ordered_idom
 
-lemmas linorder_neqE_ordered_idom =
- linorder_neqE[where 'a = "?'b::ordered_idom"]
+lemma linorder_neqE_ordered_idom:
+  fixes x y :: "'a :: ordered_idom"
+  assumes "x \<noteq> y" obtains "x < y" | "y < x"
+  using assms by (rule linorder_neqE)
 
 lemma eq_add_iff1:
   "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))"