# HG changeset patch
# User krauss
# Date 1248093279 -7200
# Node ID 1fb676ab8d9937a6bde7dcd73529eebf69a66f54
# Parent  b916fb3f9136e16c700e674943c3ee112905cfc5
no SAME exceptions in uncritical code

diff -r b916fb3f9136 -r 1fb676ab8d99 src/HOL/Tools/Function/fundef_core.ML
--- a/src/HOL/Tools/Function/fundef_core.ML	Mon Jul 20 15:24:31 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_core.ML	Mon Jul 20 14:34:39 2009 +0200
@@ -176,7 +176,7 @@
     end
 
 
-(* lowlevel term function *)
+(* lowlevel term function. FIXME: remove *)
 fun abstract_over_list vs body =
   let
     fun abs lev v tm =
@@ -184,12 +184,10 @@
       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.SAME => u)
-              handle Same.SAME => t $ abs lev v u)
-        | _ => raise Same.SAME);
+        | t $ u => abs lev v t $ abs lev v u
+        | t => t);
   in
-    fold_index (fn (i, v) => fn t => abs i v t handle Same.SAME => t) vs body
+    fold_index (fn (i, v) => fn t => abs i v t) vs body
   end