Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid catch-all exception handler, presumably TERM was meant here;
authorwenzelm
Wed, 12 Jan 2011 15:07:29 +0100
changeset 41519 0940fff556a6
parent 41518 bcacc58902fa
child 41520 3470b54e95d6
avoid catch-all exception handler, presumably TERM was meant here;
src/HOL/Nominal/nominal_fresh_fun.ML file | annotate | diff | comparison | revisions 
--- 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';
isabelle