src/HOL/MiniML/W.thy

 (* type inference algorithm W *)
 
 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),   
 	                         n + (min_new_bound_tv (A!i)) )  
 	              else None)"