--- a/Nominal/Perm.thy	Tue Apr 20 08:57:13 2010 +0200
+++ b/Nominal/Perm.thy	Tue Apr 20 09:02:22 2010 +0200
@@ -16,7 +16,7 @@
 *}
 
 ML {*
-fun prove_perm_empty lthy induct perm_def perm_frees =
+fun prove_perm_zero lthy induct perm_def perm_frees =
 let
   val perm_types = map fastype_of perm_frees;
   val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
@@ -36,7 +36,7 @@
 *}
 
 ML {*
-fun prove_perm_append lthy induct perm_def perm_frees =
+fun prove_perm_plus lthy induct perm_def perm_frees =
 let
   val pi1 = Free ("pi1", @{typ perm});
   val pi2 = Free ("pi2", @{typ perm});
@@ -86,8 +86,9 @@
 *}
 
 ML {*
-(* equation for permutation function for one constructor *)
-fun perm_eq_constr thy dt_descr sorts permute_fns i (cnstr_name, dts) =
+(* equation for permutation function for one constructor;
+   i is the index of the correspodning datatype *)
+fun perm_eq_constr dt_descr sorts permute_fns i (cnstr_name, dts) =
 let
   val pi = Free ("p", @{typ perm})
   val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts
@@ -120,7 +121,7 @@
   val permute_fns = perm_fn_names ~~ perm_types
 
   fun perm_eq (i, (_, _, constrs)) = 
-    map (perm_eq_constr thy dt_descr sorts permute_fns i) constrs;
+    map (perm_eq_constr dt_descr sorts permute_fns i) constrs;
 
   val perm_eqs = maps perm_eq dt_descr;
 
@@ -131,21 +132,21 @@
     Primrec.add_primrec
       (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy;
     
-  val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, dt_nos);
-  val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, dt_nos)
+  val perm_zero_thms = List.take (prove_perm_zero lthy' induct perm_ldef perm_frees, dt_nos);
+  val perm_plus_thms = List.take (prove_perm_plus lthy' induct perm_ldef perm_frees, dt_nos)
   val perms_name = space_implode "_" perm_fn_names
   val perms_zero_bind = Binding.name (perms_name ^ "_zero")
-  val perms_append_bind = Binding.name (perms_name ^ "_append")
+  val perms_plus_bind = Binding.name (perms_name ^ "_plus")
   fun tac _ (_, simps, _) =
     (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps));
   fun morphism phi (dfs, simps, fvs) =
     (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs);
   in
     lthy'
-    |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms))
-    |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms))
+    |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms))
+    |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms))
     |> Class_Target.prove_instantiation_exit_result morphism tac 
-         (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees)
+         (perm_ldef, (perm_zero_thms @ perm_plus_thms), perm_frees)
   end
 *}