diff -r 89f162de39cf -r 9b8547a9496a src/HOL/MiniML/W.thy
--- 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),