diff -r 1810b1ade437 -r 47ee18b6ae32 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Mon Mar 01 12:30:55 2010 +0100
+++ b/src/Sequents/LK0.thy	Mon Mar 01 13:42:31 2010 +0100
@@ -122,8 +122,7 @@
   The: "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==>
           $H |- $E, P(THE x. P(x)), $F"
 
-constdefs
-  If :: "[o, 'a, 'a] => 'a"   ("(if (_)/ then (_)/ else (_))" 10)
+definition If :: "[o, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) where 
    "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"