--- a/src/HOL/MiniML/W.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/W.thy Fri Jul 24 13:19:38 1998 +0200
@@ -17,7 +17,7 @@
consts
W :: [expr, ctxt, nat] => result_W
-primrec W expr
+primrec
"W (Var i) A n =
(if i < length A then Some( id_subst,
bound_typ_inst (%b. TVar(b+n)) (A!i),