# HG changeset patch
# User nipkow
# Date 818448495 -3600
# Node ID 5d909faf0e04320fa8d48f49cb8cb50d2bdaab93
# Parent  1f00494e37a5ac6cd3afa7086e06b2d24ae452af
Introduced Monad syntax Pat := Val; Cont

diff -r 1f00494e37a5 -r 5d909faf0e04 src/HOL/MiniML/I.ML
--- a/src/HOL/MiniML/I.ML	Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/I.ML	Fri Dec 08 19:48:15 1995 +0100
@@ -115,7 +115,7 @@
     addss !simpset) 1);
 by (dres_inst_tac [("e","expr1")] (sym RS W_var_geD) 1);
 by ((dtac new_tv_subst_tel 1) THEN (atac 1));
-by ((dres_inst_tac [("a","$ s a")] new_tv_list_le 1) THEN (atac 1));
+by ((dres_inst_tac [("ts","$ s a")] new_tv_list_le 1) THEN (atac 1));
 by ((dtac new_tv_subst_tel 1) THEN (atac 1));
 by (fast_tac (HOL_cs addDs [new_tv_W] addss 
     (!simpset addsimps [subst_comp_tel])) 1);
diff -r 1f00494e37a5 -r 5d909faf0e04 src/HOL/MiniML/I.thy
--- a/src/HOL/MiniML/I.thy	Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/I.thy	Fri Dec 08 19:48:15 1995 +0100
@@ -8,17 +8,16 @@
 I = W +
 
 consts
-	I :: [expr, type_expr list, nat, subst] => result_W
+	I :: [expr, typ list, nat, subst] => result_W
 
 primrec I expr
         I_Var	"I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
                                     else Fail)"
-        I_Abs	"I (Abs e) a n s = I e ((TVar n)#a) (Suc n) s   bind
-                                   (%(s,t,m). Ok(s, Fun (TVar n) t, m) )"
+        I_Abs	"I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
+                                     Ok(s, TVar n -> t, m) )"
         I_App	"I (App e1 e2) a n s =
- 		 I e1 a n s   bind
-		 (%(s1,t1,m1). I e2 a m1 s1  bind   
-		 (%(s2,t2,m2). mgu ($s2 t1) (Fun ($s2 t2) (TVar m2)) bind
-		 (%u. Ok($u o s2, TVar m2, Suc m2) ) ))"
-
+ 		   ( (s1,t1,m1) := I e1 a n s;
+		     (s2,t2,m2) := I e2 a m1 s1;
+		     u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
+		     Ok($u o s2, TVar m2, Suc m2) )"
 end
diff -r 1f00494e37a5 -r 5d909faf0e04 src/HOL/MiniML/Maybe.thy
--- a/src/HOL/MiniML/Maybe.thy	Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/Maybe.thy	Fri Dec 08 19:48:15 1995 +0100
@@ -15,4 +15,7 @@
 defs
   bind_def "m bind f == case m of Ok r => f r | Fail => Fail"
 
+syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
+translations "P := E; F" == "E bind (%P.F)"
+
 end
diff -r 1f00494e37a5 -r 5d909faf0e04 src/HOL/MiniML/MiniML.thy
--- a/src/HOL/MiniML/MiniML.thy	Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/MiniML.thy	Fri Dec 08 19:48:15 1995 +0100
@@ -14,9 +14,9 @@
 
 (* type inference rules *)
 consts
-	has_type :: "(type_expr list * expr * type_expr)set"
+	has_type :: "(typ list * expr * typ)set"
 syntax
-        "@has_type" :: [type_expr list, expr, type_expr] => bool
+        "@has_type" :: [typ list, expr, typ] => bool
                        ("((_) |-/ (_) :: (_))" 60)
 translations 
         "a |- e :: t" == "(a,e,t):has_type"
@@ -24,8 +24,8 @@
 inductive "has_type"
 intrs
 	VarI "[| n < length a |] ==> a |- Var n :: nth n a"
-	AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: Fun t1 t2"
-	AppI "[| a |- e1 :: Fun t2 t1; a |- e2 :: t2 |] 
+	AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
+	AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] 
      	      ==> a |- App e1 e2 :: t1"
 
 end
diff -r 1f00494e37a5 -r 5d909faf0e04 src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/Type.ML	Fri Dec 08 19:48:15 1995 +0100
@@ -13,18 +13,18 @@
 
 (* application of id_subst does not change type expression *)
 goalw thy [id_subst_def]
-  "$ id_subst = (%t::type_expr.t)";
+  "$ id_subst = (%t::typ.t)";
 by (rtac ext 1);
-by (type_expr.induct_tac "t" 1);
+by (typ.induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "app_subst_id_te";
 Addsimps [app_subst_id_te];
 
 (* application of id_subst does not change list of type expressions *)
 goalw thy [app_subst_list]
-  "$ id_subst = (%l::type_expr list.l)";
+  "$ id_subst = (%ts::typ list.ts)";
 by (rtac ext 1); 
-by (list.induct_tac "l" 1);
+by (list.induct_tac "ts" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "app_subst_id_tel";
 Addsimps [app_subst_id_tel];
@@ -60,14 +60,14 @@
 
 (* composition of substitutions *)
 goal thy
-  "$ g ($ f t::type_expr) = $ (%x. $ g (f x) ) t";
-by (type_expr.induct_tac "t" 1);
+  "$ g ($ f t::typ) = $ (%x. $ g (f x) ) t";
+by (typ.induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "subst_comp_te";
 
 goalw thy [app_subst_list]
-  "$ g ($ f l::type_expr list) = $ (%x. $ g (f x)) l";
-by (list.induct_tac "l" 1);
+  "$ g ($ f ts::typ list) = $ (%x. $ g (f x)) ts";
+by (list.induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case x#xl *)
@@ -82,7 +82,7 @@
 qed "app_subst_Nil";
 
 goalw thy [app_subst_list]
-  "$ s (x#l) = ($ s x)#($ s l)";
+  "$ s (t#ts) = ($ s t)#($ s ts)";
 by (Simp_tac 1);
 qed "app_subst_Cons";
 
@@ -95,7 +95,7 @@
 qed "new_tv_TVar";
 
 goalw thy [new_tv_def]
-  "new_tv n (Fun t1 t2) = (new_tv n t1 & new_tv n t2)";
+  "new_tv n (t1 -> t2) = (new_tv n t1 & new_tv n t2)";
 by (fast_tac (HOL_cs addss !simpset) 1);
 qed "new_tv_Fun";
 
@@ -105,7 +105,7 @@
 qed "new_tv_Nil";
 
 goalw thy [new_tv_def]
-  "new_tv n (x#l) = (new_tv n x & new_tv n l)";
+  "new_tv n (t#ts) = (new_tv n t & new_tv n ts)";
 by (fast_tac (HOL_cs addss !simpset) 1);
 qed "new_tv_Cons";
 
@@ -142,23 +142,23 @@
 
 (* substitution affects only variables occurring freely *)
 goal thy
-  "new_tv n (t::type_expr) --> $(%x. if x=n then t' else s x) t = $s t";
-by (type_expr.induct_tac "t" 1);
+  "new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
+by (typ.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "subst_te_new_tv";
 Addsimps [subst_te_new_tv];
 
 goal thy
-  "new_tv n (a::type_expr list) --> $(%x. if x=n then t else s x) a = $s a";
-by (list.induct_tac "a" 1);
+  "new_tv n (ts::typ list) --> $(%x. if x=n then t else s x) ts = $s ts";
+by (list.induct_tac "ts" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "subst_tel_new_tv";
 Addsimps [subst_tel_new_tv];
 
 (* all greater variables are also new *)
 goal thy
-  "n<=m --> new_tv n (t::type_expr) --> new_tv m t";
-by (type_expr.induct_tac "t" 1);
+  "n<=m --> new_tv n (t::typ) --> new_tv m t";
+by (typ.induct_tac "t" 1);
 (* case TVar n *)
 by( fast_tac (HOL_cs addIs [less_le_trans] addss !simpset) 1);
 (* case Fun t1 t2 *)
@@ -167,8 +167,8 @@
 Addsimps [lessI RS less_imp_le RS new_tv_le];
 
 goal thy 
-  "n<=m --> new_tv n (a::type_expr list) --> new_tv m a";
-by( list.induct_tac "a" 1);
+  "n<=m --> new_tv n (ts::typ list) --> new_tv m ts";
+by( list.induct_tac "ts" 1);
 (* case [] *)
 by(Simp_tac 1);
 (* case a#al *)
@@ -195,25 +195,25 @@
 qed "new_tv_subst_var";
 
 goal thy
-  "new_tv n s --> new_tv n (t::type_expr) --> new_tv n ($ s t)";
-by (type_expr.induct_tac "t" 1);
+  "new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)";
+by (typ.induct_tac "t" 1);
 by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst]))));
 bind_thm ("new_tv_subst_te",result() RS mp RS mp);
 Addsimps [new_tv_subst_te];
 
-goal thy 
-  "new_tv n s --> new_tv n (a::type_expr list) --> new_tv n ($ s a)";
+goal thy
+  "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
 by( simp_tac (!simpset addsimps [new_tv_list]) 1);
-by (list.induct_tac "a" 1);
+by (list.induct_tac "ts" 1);
 by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst]))));
 bind_thm ("new_tv_subst_tel",result() RS mp RS mp);
 Addsimps [new_tv_subst_tel];
 
 (* auxilliary lemma *)
 goal thy
-  "new_tv n a --> new_tv (Suc n) ((TVar n)#a)";
+  "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
 by( simp_tac (!simpset addsimps [new_tv_list]) 1);
-by (list.induct_tac "a" 1);
+by (list.induct_tac "ts" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "new_tv_Suc_list";
 
@@ -241,8 +241,8 @@
 Addsimps [new_tv_not_free_tv];
 
 goal thy
-  "(t::type_expr) mem l --> free_tv t <= free_tv l";
-by (list.induct_tac "l" 1);
+  "(t::typ) mem ts --> free_tv t <= free_tv ts";
+by (list.induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case x#xl *)
@@ -255,8 +255,8 @@
    structure the substitutions coincide on the free type variables
    occurring in the type structure *)
 goal thy
-  "$ s1 (t::type_expr) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n";
-by (type_expr.induct_tac "t" 1);
+  "$ s1 (t::typ) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n";
+by (typ.induct_tac "t" 1);
 (* case TVar n *)
 by (fast_tac (HOL_cs addss !simpset) 1);
 (* case Fun t1 t2 *)
@@ -264,8 +264,8 @@
 bind_thm ("eq_subst_te_eq_free",result() RS mp RS mp);
 
 goal thy
-  "(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::type_expr) = $ s2 t";
-by (type_expr.induct_tac "t" 1);
+  "(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::typ) = $ s2 t";
+by (typ.induct_tac "t" 1);
 (* case TVar n *)
 by (fast_tac (HOL_cs addss !simpset) 1);
 (* case Fun t1 t2 *)
@@ -273,8 +273,8 @@
 bind_thm ("eq_free_eq_subst_te",result() RS mp);
 
 goal thy
-  "$ s1 (l::type_expr list) = $ s2 l --> n:(free_tv l) --> s1 n = s2 n";
-by (list.induct_tac "l" 1);
+  "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
+by (list.induct_tac "ts" 1);
 (* case [] *)
 by (fast_tac (HOL_cs addss !simpset) 1);
 (* case x#xl *)
@@ -282,8 +282,8 @@
 bind_thm ("eq_subst_tel_eq_free",result() RS mp RS mp);
 
 goal thy
-  "(!n. n:(free_tv l) --> s1 n = s2 n) --> $s1 (l::type_expr list) = $s2 l";
-by (list.induct_tac "l" 1); 
+  "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
+by (list.induct_tac "ts" 1); 
 (* case [] *)
 by (fast_tac (HOL_cs addss !simpset) 1);
 (* case x#xl *)
@@ -315,8 +315,8 @@
 qed "free_tv_subst_var";
 
 goal thy 
-     "free_tv ($ s (e::type_expr)) <= cod s Un free_tv e";
-by( type_expr.induct_tac "e" 1);
+     "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
+by( typ.induct_tac "t" 1);
 (* case TVar n *)
 by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
 (* case Fun t1 t2 *)
@@ -324,8 +324,8 @@
 qed "free_tv_app_subst_te";     
 
 goal thy 
-     "free_tv ($ s (l::type_expr list)) <= cod s Un free_tv l";
-by( list.induct_tac "l" 1);
+     "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
+by( list.induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case a#al *)
@@ -334,8 +334,7 @@
 qed "free_tv_app_subst_tel";
 
 goalw thy [free_tv_subst,dom_def] 
-     "free_tv (%u::nat. $ s1 ($ s2 (s3 u)) :: type_expr ) <=   \ 
+     "free_tv (%u::nat. $ s1 ($ s2 (s3 u)) :: typ) <=   \ 
 \     free_tv s1 Un free_tv s2 Un free_tv s3";
 by( fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD,free_tv_subst_var RS subsetD] addss (!simpset addsimps [cod_def,dom_def])) 1);
 qed "free_tv_comp_subst";    
-
diff -r 1f00494e37a5 -r 5d909faf0e04 src/HOL/MiniML/Type.thy
--- a/src/HOL/MiniML/Type.thy	Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/Type.thy	Fri Dec 08 19:48:15 1995 +0100
@@ -14,14 +14,14 @@
 
 (* type expressions *)
 datatype
-	type_expr = TVar nat | Fun type_expr type_expr
+	typ = TVar nat | "->" typ typ (infixr 70)
 
 (* type variable substitution *)
 types
-	subst = nat => type_expr
+	subst = nat => typ
 
 arities
-	type_expr::type_struct
+	typ::type_struct
 	list::(type_struct)type_struct
 	fun::(term,type_struct)type_struct
 
@@ -39,7 +39,7 @@
 
 rules
 	app_subst_TVar  "$ s (TVar n) = s n" 
-	app_subst_Fun	"$ s (Fun t1 t2) = Fun ($ s t1) ($ s t2)" 
+	app_subst_Fun	"$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
 defs
         app_subst_list	"$ s == map ($ s)"
   
@@ -49,7 +49,7 @@
 
 rules
 	free_tv_TVar	"free_tv (TVar m) = {m}"
-	free_tv_Fun	"free_tv (Fun t1 t2) = (free_tv t1) Un (free_tv t2)"
+	free_tv_Fun	"free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
 	free_tv_Nil	"free_tv [] = {}"
 	free_tv_Cons	"free_tv (x#l) = (free_tv x) Un (free_tv l)"
 
@@ -78,12 +78,12 @@
 
 (* unification algorithm mgu *)
 consts
-	mgu :: [type_expr,type_expr] => subst maybe
+	mgu :: [typ,typ] => subst maybe
 rules
-	mgu_eq 	 "mgu t1 t2 = Ok u ==> $ u t1 = $ u t2"
-	mgu_mg 	 "[| (mgu t1 t2) = Ok u; $ s t1 = $ s t2 |] ==>
-		  ? r. s = ($ r) o u"
-	mgu_Ok	 "$ s t1 = $ s t2 ==> ? u. mgu t1 t2 = Ok u"
+	mgu_eq 	 "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
+	mgu_mg 	 "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
+		  ? r. s = $r o u"
+	mgu_Ok	 "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"
 	mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"
 
 end
diff -r 1f00494e37a5 -r 5d909faf0e04 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/W.ML	Fri Dec 08 19:48:15 1995 +0100
@@ -37,7 +37,7 @@
 by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);
 by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1);
 by (rtac (app_subst_Fun RS subst) 1);
-by (res_inst_tac [("t","$ sc (Fun tb (TVar nb))"),("s","$ sc ($ sb ta)")] subst 1);
+by (res_inst_tac [("t","$ sc (tb -> (TVar nb))"),("s","$ sc ($ sb ta)")] subst 1);
 by (Asm_full_simp_tac 1);
 by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym]) 1);
 by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1));
@@ -255,7 +255,7 @@
 by (eresolve_tac has_type_casesE 1);
 by (eres_inst_tac [("x","s'")] allE 1);
 by (eres_inst_tac [("x","a")] allE 1);
-by (eres_inst_tac [("x","Fun t2 t'")] allE 1);
+by (eres_inst_tac [("x","t2 -> t'")] allE 1);
 by (eres_inst_tac [("x","n")] allE 1);
 by (safe_tac HOL_cs);
 by (eres_inst_tac [("x","r")] allE 1);
@@ -275,10 +275,10 @@
   "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
 \        else ra x)) ($ sa t) = \
 \  $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
-\        else ra x)) (Fun ta (TVar ma))" 1);
+\        else ra x)) (ta -> (TVar ma))" 1);
 by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
 \   (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"),
-    ("s","Fun ($ ra ta) t'")] ssubst 2);
+    ("s","($ ra ta) -> t'")] ssubst 2);
 by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2);
 br eq_free_eq_subst_te 2;  
 by (strip_tac 2);
@@ -290,7 +290,7 @@
 by (asm_simp_tac (!simpset addsimps [not_free_impl_id]
     setloop (split_tac [expand_if])) 3);
 (* na : free_tv sa *)
-by (dres_inst_tac [("l1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
+by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
 bd eq_subst_tel_eq_free 2;
 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
 by (Asm_simp_tac 2); 
@@ -324,7 +324,7 @@
 by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
 (* case na : free_tv t - free_tv sa *)
 by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
-by (dres_inst_tac [("l1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
+by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
 bd eq_subst_tel_eq_free 2;
 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
 by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,not_disj]) 2);
@@ -343,7 +343,7 @@
 by (dres_inst_tac [("x","ma")] fun_cong 2);
 by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
 by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1);
-by (res_inst_tac [("l2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN 
+by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN 
     (2,trans)) 1);
 by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
 br eq_free_eq_subst_tel 1;
diff -r 1f00494e37a5 -r 5d909faf0e04 src/HOL/MiniML/W.thy
--- a/src/HOL/MiniML/W.thy	Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/W.thy	Fri Dec 08 19:48:15 1995 +0100
@@ -9,20 +9,20 @@
 W = MiniML + 
 
 types 
-        result_W = "(subst * type_expr * nat)maybe"
+        result_W = "(subst * typ * nat)maybe"
 
 (* type inference algorithm W *)
 consts
-	W :: [expr, type_expr list, nat] => result_W
+	W :: [expr, typ list, nat] => result_W
 
 primrec W expr
   W_Var	"W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
 		          else Fail)"
-  W_Abs	"W (Abs e) a n = W e ((TVar n)#a) (Suc n)    bind   
-		         (%(s,t,m). Ok(s, Fun (s n) t, m) )"
+  W_Abs	"W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
+		           Ok(s, (s n) -> t, m) )"
   W_App	"W (App e1 e2) a n =
- 		 W e1 a n    bind
-		 (%(s1,t1,m1). W e2 ($ s1 a) m1   bind   
-		 (%(s2,t2,m2). mgu ($ s2 t1) (Fun t2 (TVar m2)) bind
-		 (%u. Ok( ($ u) o (($ s2) o s1), $ u (TVar m2), Suc m2) )))"
+ 		 ( (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) )"
 end