diff -r 80e2fb39332b -r de89c95c5377 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Tue Apr 10 15:21:07 2012 +0100
+++ b/Nominal/Nominal2.thy	Tue Apr 10 15:22:16 2012 +0100
@@ -352,33 +352,38 @@
 
   val _ = trace_msg (K "Defining the quotient constants...")
   val qconstrs_descrs =
-    (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) (get_cnstrs dts) raw_all_cns
+    (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) 
+      (get_cnstrs dts) raw_all_cns
 
   val qbns_descr =
-    map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) bn_funs raw_bns
+    map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) bn_funs raw_bns
 
   val qfvs_descr = 
-    map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs
+    map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_fvs
 
   val qfv_bns_descr = 
-    map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_fv_bns
+    map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) 
+      bn_funs raw_fv_bns
 
   val qalpha_bns_descr = 
     let
       val AlphaResult {alpha_bn_trms, ...} = alpha_result 
     in
-      map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn)) bn_funs  alpha_bn_trms
+      map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) 
+        bn_funs  alpha_bn_trms
     end
 
   val qperm_descr =
-    map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs
+    map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, @{thm TrueI})) 
+      qty_names raw_perm_funs
 
   val qsize_descr =
-    map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms
+    map2 (fn n => fn t => ("size_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_size_trms
 
   val qperm_bn_descr = 
-    map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_perm_bns
-     
+    map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) 
+      bn_funs raw_perm_bns
+
   val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), 
     lthy8) = 
       lthy7