# HG changeset patch
# User nipkow
# Date 849179373 -3600
# Node ID 79a2f085a7fddf6b5241754e8f706a03fec2b238
# Parent  b2326aefecbc7c578c48bc23f66f8fad186d83f1
Missing case in instantiation of Transitivity prover (negate(None)=None)

diff -r b2326aefecbc -r 79a2f085a7fd src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Thu Nov 28 10:50:43 1996 +0100
+++ b/src/HOL/Nat.ML	Thu Nov 28 12:09:33 1996 +0100
@@ -639,6 +639,7 @@
   end;
 
 fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j)
+  | negate None = None;
 
 fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
   | decomp(_$(Const("not",_)$(Const(rel,T)$lhs$rhs))) =