diff -r 90758c187861 -r 8daf6ff5e11a Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Wed Apr 28 07:27:28 2010 +0200
+++ b/Nominal/NewFv.thy	Wed Apr 28 08:22:20 2010 +0200
@@ -233,12 +233,13 @@
   val fv_nums = 0 upto (length fv_frees - 1)
 
   val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums);
-  val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
-  val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs)
+  
+  val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
+  val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
 
   val lthy' =
     lthy
-    |> Function.add_function fv_names fv_eqs_binds Function_Common.default_config
+    |> Function.add_function all_fv_names all_fv_eqs Function_Common.default_config
     |> by_pat_completeness_auto
     |> Local_Theory.restore
     |> termination_by (Lexicographic_Order.lexicographic_order)