# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272985171 -7200
# Node ID 04a881bf49e4b9feee4182904f22fa7e9943c952
# Parent  c615095827e9b0aa3ddad16e70ef5041aab038bd
Fix Term4 for permutation signature change

diff -r c615095827e9 -r 04a881bf49e4 Nominal/Manual/Term4.thy
--- 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 *)