# HG changeset patch
# User nipkow
# Date 1367202605 -7200
# Node ID 496c0ef8990cda1ab98b9c78f13e9481a383fced
# Parent  1006b9b08d7394d6f720d2e37402a964bf0fa972
tuned

diff -r 1006b9b08d73 -r 496c0ef8990c src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thy	Mon Apr 29 04:20:42 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Mon Apr 29 04:30:05 2013 +0200
@@ -27,9 +27,7 @@
 
 definition "x < (y::const) = (x \<le> y & \<not> y \<le> x)"
 
-fun sup_const where
-"Const i \<squnion> Const j = (if i=j then Const i else Any)" |
-"_ \<squnion> _ = Any"
+fun sup_const where "x \<squnion> y = (if x=y then x else Any)"
 
 definition "\<top> = Any"