# HG changeset patch
# User wenzelm
# Date 1294841249 -3600
# Node ID 0940fff556a6372ff38ca2e4aa0151c9aae392fa
# Parent  bcacc58902fa5ddfa57fb102badb225fa0acfa0d
avoid catch-all exception handler, presumably TERM was meant here;

diff -r bcacc58902fa -r 0940fff556a6 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Jan 12 14:34:11 2011 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Jan 12 15:07:29 2011 +0100
@@ -66,7 +66,8 @@
      (OldTerm.term_frees goal @ bvs);
 (* build the tuple *)
    val s = (Library.foldr1 (fn (v, s) =>
-     HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs) handle _ => HOLogic.unit ;  (* FIXME avoid handle _ *)
+       HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs)
+     handle TERM _ => HOLogic.unit;
    val fs_name_thm = get_dyn_thm thy ("fs_"^atom_basename^"1") atom_basename;
    val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    val exists_fresh' = at_name_inst_thm RS at_exists_fresh';