# 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