# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1283013407 -28800
# Node ID 6b51117b89552cd225ad728d585cc5d717d3c38f
# Parent  b9d9c45402653c560aa0b8832c722580553b12de
fiexed problem with constructors that have no arguments

diff -r b9d9c4540265 -r 6b51117b8955 Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Sun Aug 29 00:09:45 2010 +0800
+++ b/Nominal/Ex/Let.thy	Sun Aug 29 00:36:47 2010 +0800
@@ -6,6 +6,8 @@
 
 atom_decl name
 
+declare [[STEPS = 29]]
+
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
diff -r b9d9c4540265 -r 6b51117b8955 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Sun Aug 29 00:09:45 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sun Aug 29 00:36:47 2010 +0800
@@ -39,7 +39,7 @@
 apply(rule single_let.induct)
 apply(rule supports_finite)
 apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un)
+apply(simp only: finite_supp supp_Pair finite_Un, simp)
 apply(rule supports_finite)
 apply(rule single_let.supports)
 apply(simp only: finite_supp supp_Pair finite_Un, simp)
diff -r b9d9c4540265 -r 6b51117b8955 Nominal/nominal_dt_supp.ML
--- a/Nominal/nominal_dt_supp.ML	Sun Aug 29 00:09:45 2010 +0800
+++ b/Nominal/nominal_dt_supp.ML	Sun Aug 29 00:36:47 2010 +0800
@@ -21,7 +21,8 @@
 let  
   val vs = fresh_args ctxt qtrm
   val rhs = list_comb (qtrm, vs)
-  val lhs = mk_supp (foldl1 HOLogic.mk_prod vs)
+  val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"}
+    |> mk_supp
 in
   mk_supports lhs rhs
   |> HOLogic.mk_Trueprop