# HG changeset patch
# User wenzelm
# Date 1247772489 -7200
# Node ID d7f58d97fa96e5d68b69d10fe8b1fa4d3948f4ac
# Parent  9abf5d66606e6ece4850f8b7c8d09b502c327c64
use structure Same;

diff -r 9abf5d66606e -r d7f58d97fa96 src/HOL/Tools/Function/fundef_core.ML
--- a/src/HOL/Tools/Function/fundef_core.ML	Thu Jul 16 21:00:09 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_core.ML	Thu Jul 16 21:28:09 2009 +0200
@@ -179,16 +179,17 @@
 (* lowlevel term function *)
 fun abstract_over_list vs body =
   let
-    exception SAME;
     fun abs lev v tm =
       if v aconv tm then Bound lev
       else
         (case tm of
           Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
-        | t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u)
-        | _ => raise SAME);
+        | t $ u =>
+            (abs lev v t $ (abs lev v u handle Same.SAME => u)
+              handle Same.SAME => t $ abs lev v u)
+        | _ => raise Same.SAME);
   in
-    fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body
+    fold_index (fn (i, v) => fn t => abs i v t handle Same.SAME => t) vs body
   end