1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Jun 13 10:44:35 2007 +0200
1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Jun 13 11:16:24 2007 +0200
1.3 @@ -86,9 +86,8 @@
1.4 val vs = filter (fn t => is_of_fs_name (fastype_of1 (Ts, t)))
1.5 (term_frees goal @ bvs);
1.6 (* build the tuple *)
1.7 - val s = Library.foldr1 (fn (v, s) =>
1.8 - HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
1.9 - vs;
1.10 + val s = (Library.foldr1 (fn (v, s) =>
1.11 + HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs) handle _ => HOLogic.unit ;
1.12 val fs_name_thm = get_dyn_thm thy ("fs_"^atom_basename^"1") atom_basename;
1.13 val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
1.14 val exists_fresh' = at_name_inst_thm RS at_exists_fresh';