# HG changeset patch
# User nipkow
# Date 818677491 -3600
# Node ID b72ccd1cff02ce9558e715bdbc2d12d62fbf3eb5
# Parent  0c439768f45ced7f95f065d7b15082cad659aedd
layout

diff -r 0c439768f45c -r b72ccd1cff02 src/HOL/MiniML/W.thy
--- a/src/HOL/MiniML/W.thy	Sat Dec 09 13:36:11 1995 +0100
+++ b/src/HOL/MiniML/W.thy	Mon Dec 11 11:24:51 1995 +0100
@@ -22,7 +22,7 @@
 		           Ok(s, (s n) -> t, m) )"
   W_App	"W (App e1 e2) a n =
  		 ( (s1,t1,m1) := W e1 a n;
-		   (s2,t2,m2) := W e2 ($ s1 a) m1;
-		   u := mgu ($ s2 t1) (t2 -> (TVar m2));
-		   Ok( ($ u) o (($ s2) o s1), $ u (TVar m2), Suc m2) )"
+		   (s2,t2,m2) := W e2 ($s1 a) m1;
+		   u := mgu ($s2 t1) (t2 -> (TVar m2));
+		   Ok( $u o $s2 o s1, $u (TVar m2), Suc m2) )"
 end