src/ZF/Coind/Types.thy
changeset 6068 2d8f3e1f1151
parent 6046 2c8a8be36c94
child 6112 5e4871c5136b
--- a/src/ZF/Coind/Types.thy	Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/Coind/Types.thy	Thu Jan 07 10:56:05 1999 +0100
@@ -33,7 +33,7 @@
 
 primrec (*lookup up identifiers in the type environment*)
   "te_app (te_emp,x) = 0"
-  "te_app (te_owr(te,y,t),x) = if(x=y, t, te_app(te,x))"
+  "te_app (te_owr(te,y,t),x) = (if x=y then t else te_app(te,x))"
 
 end