--- a/Nominal/nominal_dt_rawfuns.ML	Tue Jun 01 15:46:07 2010 +0200
+++ b/Nominal/nominal_dt_rawfuns.ML	Wed Jun 02 11:37:51 2010 +0200
@@ -226,6 +226,9 @@
   val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
   val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
 
+  val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) ((flat fv_eqs) @ (flat fv_bn_eqs))))
+
+
   val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
     Function_Common.default_config (pat_completeness_simp constr_thms) lthy
 
@@ -255,29 +258,31 @@
 end
 
 fun raw_prove_eqvt consts ind_thms simps ctxt =
-let 
-  val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
-  val p = Free (p, @{typ perm})
-  val arg_tys = 
-    consts
-    |> map fastype_of
-    |> map domain_type 
-  val (arg_names, ctxt'') = Variable.variant_fixes (replicate (length arg_tys) "") ctxt'
-  val args = map Free (arg_names ~~ arg_tys)
-  val goals = map2 (mk_eqvt_goal p) consts args
-  val insts = map (single o SOME) arg_names
-  val const_names = map (fst o dest_Const) consts
-  fun tac ctxt = 
-    Object_Logic.full_atomize_tac
-    THEN' InductTacs.induct_rules_tac ctxt insts ind_thms 
-    THEN_ALL_NEW   
-      (asm_full_simp_tac (HOL_basic_ss addsimps simps)
-       THEN' Nominal_Permeq.eqvt_tac ctxt simps const_names
-       THEN' asm_simp_tac HOL_basic_ss)
-in
-  Goal.prove_multi ctxt' [] [] goals (fn {context, ...} => (HEADGOAL (tac context)))
-  |> ProofContext.export ctxt'' ctxt
-end
+  if null consts then []
+  else
+    let 
+      val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
+      val p = Free (p, @{typ perm})
+      val arg_tys = 
+        consts
+        |> map fastype_of
+        |> map domain_type 
+      val (arg_names, ctxt'') = Variable.variant_fixes (replicate (length arg_tys) "") ctxt'
+      val args = map Free (arg_names ~~ arg_tys)
+      val goals = map2 (mk_eqvt_goal p) consts args
+      val insts = map (single o SOME) arg_names
+      val const_names = map (fst o dest_Const) consts
+      fun tac ctxt = 
+        Object_Logic.full_atomize_tac
+        THEN' InductTacs.induct_rules_tac ctxt insts ind_thms 
+        THEN_ALL_NEW   
+          (asm_full_simp_tac (HOL_basic_ss addsimps simps)
+           THEN' Nominal_Permeq.eqvt_tac ctxt simps const_names
+           THEN' asm_simp_tac HOL_basic_ss)
+    in
+      Goal.prove_multi ctxt' [] [] goals (fn {context, ...} => (HEADGOAL (tac context)))
+      |> ProofContext.export ctxt'' ctxt
+    end
 
 end (* structure *)