src/HOL/Nominal/nominal_fresh_fun.ML
changeset 41519 0940fff556a6
parent 39557 fe5722fce758
child 42361 23f352990944
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Jan 12 14:34:11 2011 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Jan 12 15:07:29 2011 +0100
     1.3 @@ -66,7 +66,8 @@
     1.4       (OldTerm.term_frees goal @ bvs);
     1.5  (* build the tuple *)
     1.6     val s = (Library.foldr1 (fn (v, s) =>
     1.7 -     HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs) handle _ => HOLogic.unit ;  (* FIXME avoid handle _ *)
     1.8 +       HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs)
     1.9 +     handle TERM _ => HOLogic.unit;
    1.10     val fs_name_thm = get_dyn_thm thy ("fs_"^atom_basename^"1") atom_basename;
    1.11     val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    1.12     val exists_fresh' = at_name_inst_thm RS at_exists_fresh';