| changeset 1376 | 92f83b9d17e1 |
| parent 1300 | c7a8f374339b |
| child 1400 | 5d909faf0e04 |
--- a/src/HOL/MiniML/W.thy Thu Nov 30 12:58:44 1995 +0100 +++ b/src/HOL/MiniML/W.thy Fri Dec 01 12:03:13 1995 +0100 @@ -13,7 +13,7 @@ (* type inference algorithm W *) consts - W :: "[expr, type_expr list, nat] => result_W" + W :: [expr, type_expr 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)