--- a/Nominal/Perm.thy	Tue May 04 06:24:54 2010 +0100
+++ b/Nominal/Perm.thy	Tue May 04 07:22:33 2010 +0100
@@ -37,24 +37,24 @@
          p o arg
 
 *)
-fun perm_arg permute_fns p (arg_dty, arg) =
+fun perm_arg permute_fn_frees p (arg_dty, arg) =
   if Datatype_Aux.is_rec_type arg_dty 
-  then Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ p $ arg
+  then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg
   else mk_perm p arg
 *}
 
 ML {*
 (* generates the equation for the permutation function for one constructor;
    i is the index of the corresponding datatype *)
-fun perm_eq_constr dt_descr sorts permute_fns i (cnstr_name, dts) =
+fun perm_eq_constr dt_descr sorts permute_fn_frees i (cnstr_name, dts) =
 let
   val p = Free ("p", @{typ perm})
   val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts
   val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
   val args = map Free (arg_names ~~ arg_tys)
   val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i))
-  val lhs = Free (nth permute_fns i) $ p $ list_comb (cnstr, args)
-  val rhs = list_comb (cnstr, map (perm_arg permute_fns p) (dts ~~ args))
+  val lhs = (nth permute_fn_frees i) $ p $ list_comb (cnstr, args)
+  val rhs = list_comb (cnstr, map (perm_arg permute_fn_frees p) (dts ~~ args))
   val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
 in
   (Attrib.empty_binding, eq)
@@ -87,13 +87,13 @@
 ML {*
 fun prove_permute_plus lthy induct perm_defs perm_fns =
 let
-  val pi1 = Free ("p", @{typ perm})
-  val pi2 = Free ("q", @{typ perm})
+  val p = Free ("p", @{typ perm})
+  val q = Free ("q", @{typ perm})
   val perm_types = map (body_type o fastype_of) perm_fns
   val perm_indnames = Datatype_Prop.make_tnames perm_types
   
-  fun single_goal ((perm, T), x) = HOLogic.mk_eq 
-      (perm $ (mk_plus pi1 pi2) $ Free (x, T), perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
+  fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq 
+      (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T)))
 
   val goals =
     HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
@@ -123,25 +123,23 @@
   val user_full_tnames = List.take (all_full_tnames, user_dt_nos);
 
   val perm_fn_names = prefix_dt_names dt_descr sorts "permute_"
-
-  val perm_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr
-
-  val permute_fns = perm_fn_names ~~ perm_types
+  val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr
+  val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
 
   fun perm_eq (i, (_, _, constrs)) = 
-    map (perm_eq_constr dt_descr sorts permute_fns i) constrs;
+    map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs;
 
   val perm_eqs = maps perm_eq dt_descr;
 
   val lthy =
     Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy;
    
-  val ((perm_fns, perm_ldef), lthy') =
+  val ((perm_funs, perm_eq_thms), lthy') =
     Primrec.add_primrec
       (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy;
     
-  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 = prove_permute_zero lthy' induct perm_eq_thms perm_funs
+  val perm_plus_thms = prove_permute_plus lthy' induct perm_eq_thms perm_funs
   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
@@ -158,7 +156,7 @@
   |> 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_zero_thms' @ perm_plus_thms', perm_fns)
+       (perm_eq_thms, perm_zero_thms' @ perm_plus_thms', perm_funs)
 end
 *}