src/HOL/List.thy
changeset 52131 366fa32ee2a3
parent 52122 510709f8881d
child 52141 eff000cab70f
child 52143 36ffe23b25f8
     1.1 --- a/src/HOL/List.thy	Fri May 24 16:42:57 2013 +0200
     1.2 +++ b/src/HOL/List.thy	Fri May 24 17:00:46 2013 +0200
     1.3 @@ -641,7 +641,7 @@
     1.4        (case dest_case t of
     1.5          SOME (x, T, i, cont) =>
     1.6            let
     1.7 -            val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
     1.8 +            val (vs, body) = strip_abs (Envir.eta_long (map snd bound_vs) cont)
     1.9              val x' = incr_boundvars (length vs) x
    1.10              val eqs' = map (incr_boundvars (length vs)) eqs
    1.11              val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i