--- a/Nominal/Manual/Term4.thy	Tue May 04 16:44:12 2010 +0200
+++ b/Nominal/Manual/Term4.thy	Tue May 04 16:59:31 2010 +0200
@@ -10,13 +10,14 @@
   rVr4 "name"
 | rAp4 "rtrm4" "rtrm4 list"
 | rLm4 "name" "rtrm4"  --"bind (name) in (trm)"
-print_theorems
-
-thm rtrm4.recs
 
 (* there cannot be a clause for lists, as *)
 (* permutations are  already defined in Nominal (also functions, options, and so on) *)
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *}
+ML {*
+  val dtinfo = Datatype.the_info @{theory} "Term4.rtrm4";
+  val {descr, sorts, ...} = dtinfo;
+*}
+setup {* snd o (define_raw_perms descr sorts @{thm rtrm4.induct} 1) *}
 print_theorems
 
 (* "repairing" of the permute function *)