1.1 --- a/src/HOL/Tools/Function/fundef_core.ML	Thu Jul 16 21:00:09 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/fundef_core.ML	Thu Jul 16 21:28:09 2009 +0200
     1.3 @@ -179,16 +179,17 @@
     1.4  (* lowlevel term function *)
     1.5  fun abstract_over_list vs body =
     1.6    let
     1.7 -    exception SAME;
     1.8      fun abs lev v tm =
     1.9        if v aconv tm then Bound lev
    1.10        else
    1.11          (case tm of
    1.12            Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
    1.13 -        | t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u)
    1.14 -        | _ => raise SAME);
    1.15 +        | t $ u =>
    1.16 +            (abs lev v t $ (abs lev v u handle Same.SAME => u)
    1.17 +              handle Same.SAME => t $ abs lev v u)
    1.18 +        | _ => raise Same.SAME);
    1.19    in
    1.20 -    fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body
    1.21 +    fold_index (fn (i, v) => fn t => abs i v t handle Same.SAME => t) vs body
    1.22    end
    1.23  
    1.24