# HG changeset patch
# User paulson
# Date 1158589284 -7200
# Node ID 93ae490fe02cb1c4f26ee5348233d05c18ec595e
# Parent  499500b1e3484d49ad19b3724da96dcb49dc6ae1
Bug fix to prevent exception dest_Free from escaping

diff -r 499500b1e348 -r 93ae490fe02c src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Mon Sep 18 16:00:19 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Mon Sep 18 16:21:24 2006 +0200
@@ -325,8 +325,10 @@
                 map (forall_intr_vars o strip_lambdas o object_eq) defs
   in  (theory_of_thm eqth, ths)  end;
 
+fun name_of def = SOME (#1 (dest_Free (lhs_of def))) handle _ => NONE;
+
 (*A name is valid provided it isn't the name of a defined abstraction.*)
-fun valid_name defs (Free(x,T)) = not (x mem_string (map (#1 o dest_Free o lhs_of) defs))
+fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs))
   | valid_name defs _ = false;
 
 fun assume_absfuns th =