# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272950694 -3600
# Node ID 205ac2d1333980185f7eb72848a26b41ba57cabe
# Parent  be512c15daa5edfb86a4001ecf71be28ca3116d0
roll back of the last commit (there was a difference)

diff -r be512c15daa5 -r 205ac2d13339 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Tue May 04 06:05:13 2010 +0100
+++ b/Nominal/NewParser.thy	Tue May 04 06:24:54 2010 +0100
@@ -374,7 +374,7 @@
 
   (* definitions of raw permutations *)
   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
-    Local_Theory.theory_result (define_raw_perms dtinfo) lthy1;
+    Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
 
   val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
   fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
diff -r be512c15daa5 -r 205ac2d13339 Nominal/Perm.thy
--- a/Nominal/Perm.thy	Tue May 04 06:05:13 2010 +0100
+++ b/Nominal/Perm.thy	Tue May 04 06:24:54 2010 +0100
@@ -113,15 +113,14 @@
 (* defines the permutation functions for raw datatypes and
    proves that they are instances of pt
 
-   dt_nos refers to the number of "un-unfolded" datatypes
+   user_dt_nos refers to the number of "un-unfolded" datatypes
    given by the user
 *)
-fun define_raw_perms (dt_info : Datatype_Aux.info) thy =
+fun define_raw_perms (dt_info : Datatype_Aux.info) user_dt_nos thy =
 let
   val {descr as dt_descr, induct, sorts, ...} = dt_info;
-  val dt_nos = length dt_descr
   val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
-  val full_tnames = List.take (all_full_tnames, dt_nos);
+  val user_full_tnames = List.take (all_full_tnames, user_dt_nos);
 
   val perm_fn_names = prefix_dt_names dt_descr sorts "permute_"
 
@@ -135,7 +134,7 @@
   val perm_eqs = maps perm_eq dt_descr;
 
   val lthy =
-    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
+    Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy;
    
   val ((perm_fns, perm_ldef), lthy') =
     Primrec.add_primrec
@@ -143,8 +142,8 @@
     
   val perm_zero_thms = prove_permute_zero lthy' induct perm_ldef perm_fns
   val perm_plus_thms = prove_permute_plus lthy' induct perm_ldef perm_fns
-  val perm_zero_thms' = List.take (perm_zero_thms, dt_nos);
-  val perm_plus_thms' = List.take (perm_plus_thms, dt_nos)
+  val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos);
+  val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos)
   val perms_name = space_implode "_" perm_fn_names
   val perms_zero_bind = Binding.name (perms_name ^ "_zero")
   val perms_plus_bind = Binding.name (perms_name ^ "_plus")