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),