# HG changeset patch
# User narboux
# Date 1181726184 -7200
# Node ID ad690b9bca1c232920a4ffa5a20fd36870b5401e
# Parent  05f399115ba5ba60377507326d9b77a1ae643859
generate_fresh works even if there is no free variable in the goal

diff -r 05f399115ba5 -r ad690b9bca1c src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Jun 13 10:44:35 2007 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Jun 13 11:16:24 2007 +0200
@@ -86,9 +86,8 @@
    val vs = filter (fn t => is_of_fs_name (fastype_of1 (Ts, t)))
      (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;
+   val s = (Library.foldr1 (fn (v, s) =>
+     HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs) handle _ => 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';