# HG changeset patch
# User berghofe
# Date 1146232474 -7200
# Node ID 2e909d5309f46e9304c529024f93999474ed2293
# Parent  d8f2527574602c509c8f4e33e8d7af4312574ce4
Renamed "nominal" theory to "Nominal".

diff -r d8f252757460 -r 2e909d5309f4 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Fri Apr 28 15:53:47 2006 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Fri Apr 28 15:54:34 2006 +0200
@@ -1,6 +1,6 @@
 (* $Id$ *)
 
-theory nominal 
+theory Nominal 
 imports Main
 uses
   ("nominal_atoms.ML")
@@ -9,8 +9,6 @@
   ("nominal_permeq.ML")
 begin 
 
-ML {* reset NameSpace.unique_names; *}
-
 section {* Permutations *}
 (*======================*)
 
@@ -2838,4 +2836,5 @@
 method_setup finite_guess_debug =
   {* finite_gs_meth_debug *}
   {* tactic for deciding whether something has finite support including debuging facilities *}
+
 end
diff -r d8f252757460 -r 2e909d5309f4 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Fri Apr 28 15:53:47 2006 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Apr 28 15:54:34 2006 +0200
@@ -1,4 +1,9 @@
-(* $Id$ *)
+(*  Title:      HOL/Nominal/nominal_atoms.ML
+    ID:         $Id$
+    Author:     Christian Urban and Stefan Berghofer, TU Muenchen
+
+Declaration of atom types to be used in nominal datatypes.
+*)
 
 signature NOMINAL_ATOMS =
 sig
@@ -80,7 +85,7 @@
         val ab = Free ("ab", HOLogic.mk_prodT (T, T))
         val cif = Const ("HOL.If", HOLogic.boolT --> T --> T --> T);
         val cswap_akname = Const (swap_name, swapT);
-        val cswap = Const ("nominal.swap", swapT)
+        val cswap = Const ("Nominal.swap", swapT)
 
         val name = "swap_"^ak_name^"_def";
         val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -136,7 +141,7 @@
           val perm_def_name = ak_name ^ "_prm_" ^ ak_name';
           val pi = Free ("pi", mk_permT T);
           val a  = Free ("a", T');
-          val cperm = Const ("nominal.perm", mk_permT T --> T' --> T');
+          val cperm = Const ("Nominal.perm", mk_permT T --> T' --> T');
           val cperm_def = Const (Sign.full_name (sign_of thy') perm_def_name, mk_permT T --> T' --> T');
 
           val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def";
@@ -154,7 +159,7 @@
       let
         val ak_name_qu = Sign.full_name (sign_of thy5) (ak_name);
         val i_type = Type(ak_name_qu,[]);
-	val cat = Const ("nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
+	val cat = Const ("Nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
         val at_type = Logic.mk_type i_type;
         val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy5
                                   [Name "at_def",
@@ -185,10 +190,10 @@
           val x   = Free ("x", ty);
           val pi1 = Free ("pi1", mk_permT T);
           val pi2 = Free ("pi2", mk_permT T);
-          val cperm = Const ("nominal.perm", mk_permT T --> ty --> ty);
+          val cperm = Const ("Nominal.perm", mk_permT T --> ty --> ty);
           val cnil  = Const ("List.list.Nil", mk_permT T);
           val cappend = Const ("List.op @",mk_permT T --> mk_permT T --> mk_permT T);
-          val cprm_eq = Const ("nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
+          val cprm_eq = Const ("Nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
           (* nil axiom *)
           val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq 
                        (cperm $ cnil $ x, x));
@@ -217,7 +222,7 @@
         val pt_name_qu = Sign.full_name (sign_of thy7) ("pt_"^ak_name);
         val i_type1 = TFree("'x",[pt_name_qu]);
         val i_type2 = Type(ak_name_qu,[]);
-	val cpt = Const ("nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
+	val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
         val pt_type = Logic.mk_type i_type1;
         val at_type = Logic.mk_type i_type2;
         val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy7
@@ -243,7 +248,7 @@
 	  val pt_name = Sign.full_name (sign_of thy) ("pt_"^ak_name);
           val ty = TFree("'a",["HOL.type"]);
           val x   = Free ("x", ty);
-          val csupp    = Const ("nominal.supp", ty --> HOLogic.mk_setT T);
+          val csupp    = Const ("Nominal.supp", ty --> HOLogic.mk_setT T);
           val cfinites = Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T))
           
           val axiom1   = HOLogic.mk_Trueprop (HOLogic.mk_mem (csupp $ x, cfinites));
@@ -263,7 +268,7 @@
          val fs_name_qu = Sign.full_name (sign_of thy11) ("fs_"^ak_name);
          val i_type1 = TFree("'x",[fs_name_qu]);
          val i_type2 = Type(ak_name_qu,[]);
- 	 val cfs = Const ("nominal.fs", 
+ 	 val cfs = Const ("Nominal.fs", 
                                  (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
          val fs_type = Logic.mk_type i_type1;
          val at_type = Logic.mk_type i_type2;
@@ -290,9 +295,9 @@
                val x   = Free ("x", ty);
                val pi1 = Free ("pi1", mk_permT T);
 	       val pi2 = Free ("pi2", mk_permT T');                  
-	       val cperm1 = Const ("nominal.perm", mk_permT T  --> ty --> ty);
-               val cperm2 = Const ("nominal.perm", mk_permT T' --> ty --> ty);
-               val cperm3 = Const ("nominal.perm", mk_permT T  --> mk_permT T' --> mk_permT T');
+	       val cperm1 = Const ("Nominal.perm", mk_permT T  --> ty --> ty);
+               val cperm2 = Const ("Nominal.perm", mk_permT T' --> ty --> ty);
+               val cperm3 = Const ("Nominal.perm", mk_permT T  --> mk_permT T' --> mk_permT T');
 
                val ax1   = HOLogic.mk_Trueprop 
 			   (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
@@ -313,7 +318,7 @@
              val i_type0 = TFree("'a",[cp_name_qu]);
              val i_type1 = Type(ak_name_qu,[]);
              val i_type2 = Type(ak_name_qu',[]);
-	     val ccp = Const ("nominal.cp",
+	     val ccp = Const ("Nominal.cp",
                              (Term.itselfT i_type0)-->(Term.itselfT i_type1)-->
                                                       (Term.itselfT i_type2)-->HOLogic.boolT);
              val at_type  = Logic.mk_type i_type1;
@@ -344,7 +349,7 @@
 	         val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');
                  val i_type1 = Type(ak_name_qu,[]);
                  val i_type2 = Type(ak_name_qu',[]);
-	         val cdj = Const ("nominal.disjoint",
+	         val cdj = Const ("Nominal.disjoint",
                            (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
                  val at_type  = Logic.mk_type i_type1;
                  val at_type' = Logic.mk_type i_type2;
@@ -436,11 +441,11 @@
        in 
 	thy
 	|> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
-        |> AxClass.prove_arity ("nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
+        |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
         |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
         |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
         |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
-        |> AxClass.prove_arity ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
+        |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
                                     (pt_proof pt_thm_nprod)
         |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
         |> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
@@ -502,7 +507,7 @@
          thy 
          |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
          |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
-         |> AxClass.prove_arity ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
+         |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
                                      (fs_proof fs_thm_nprod) 
          |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
          |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
@@ -586,7 +591,7 @@
          |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
          |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
          |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
-         |> AxClass.prove_arity ("nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
+         |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
         end) ak_names thy) ak_names thy25;
        
      (* show that discrete nominal types are permutation types, finitely     *) 
@@ -609,7 +614,7 @@
 	     fold (fn ak_name => fn thy =>
 	     let
 	       val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
-	       val supp_def = thm "nominal.supp_def";
+	       val supp_def = thm "Nominal.supp_def";
                val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites.emptyI,defn];
                val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];      
              in  
@@ -620,7 +625,7 @@
 	     fold (fn ak_name' => (fold (fn ak_name => fn thy =>
 	     let
 	       val qu_class = Sign.full_name (sign_of thy) ("cp_"^ak_name^"_"^ak_name');
-	       val supp_def = thm "nominal.supp_def";
+	       val supp_def = thm "Nominal.supp_def";
                val simp_s = HOL_ss addsimps [defn];
                val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];      
              in  
@@ -646,32 +651,32 @@
 
        (* abbreviations for some lemmas *)
        (*===============================*)
-       val abs_fun_pi          = thm "nominal.abs_fun_pi";
-       val abs_fun_pi_ineq     = thm "nominal.abs_fun_pi_ineq";
-       val abs_fun_eq          = thm "nominal.abs_fun_eq";
-       val dj_perm_forget      = thm "nominal.dj_perm_forget";
-       val dj_pp_forget        = thm "nominal.dj_perm_perm_forget";
-       val fresh_iff           = thm "nominal.fresh_abs_fun_iff";
-       val fresh_iff_ineq      = thm "nominal.fresh_abs_fun_iff_ineq";
-       val abs_fun_supp        = thm "nominal.abs_fun_supp";
-       val abs_fun_supp_ineq   = thm "nominal.abs_fun_supp_ineq";
-       val pt_swap_bij         = thm "nominal.pt_swap_bij";
-       val pt_fresh_fresh      = thm "nominal.pt_fresh_fresh";
-       val pt_bij              = thm "nominal.pt_bij";
-       val pt_perm_compose     = thm "nominal.pt_perm_compose";
-       val pt_perm_compose'    = thm "nominal.pt_perm_compose'";
-       val perm_app            = thm "nominal.pt_fun_app_eq";
-       val at_fresh            = thm "nominal.at_fresh";
-       val at_calc             = thms "nominal.at_calc";
-       val at_supp             = thm "nominal.at_supp";
-       val dj_supp             = thm "nominal.dj_supp";
-       val fresh_left_ineq     = thm "nominal.pt_fresh_left_ineq";
-       val fresh_left          = thm "nominal.pt_fresh_left";
-       val fresh_bij_ineq      = thm "nominal.pt_fresh_bij_ineq";
-       val fresh_bij           = thm "nominal.pt_fresh_bij";
-       val pt_pi_rev           = thm "nominal.pt_pi_rev";
-       val pt_rev_pi           = thm "nominal.pt_rev_pi";
-       val fresh_fun_eqvt      = thm "nominal.fresh_fun_equiv";
+       val abs_fun_pi          = thm "Nominal.abs_fun_pi";
+       val abs_fun_pi_ineq     = thm "Nominal.abs_fun_pi_ineq";
+       val abs_fun_eq          = thm "Nominal.abs_fun_eq";
+       val dj_perm_forget      = thm "Nominal.dj_perm_forget";
+       val dj_pp_forget        = thm "Nominal.dj_perm_perm_forget";
+       val fresh_iff           = thm "Nominal.fresh_abs_fun_iff";
+       val fresh_iff_ineq      = thm "Nominal.fresh_abs_fun_iff_ineq";
+       val abs_fun_supp        = thm "Nominal.abs_fun_supp";
+       val abs_fun_supp_ineq   = thm "Nominal.abs_fun_supp_ineq";
+       val pt_swap_bij         = thm "Nominal.pt_swap_bij";
+       val pt_fresh_fresh      = thm "Nominal.pt_fresh_fresh";
+       val pt_bij              = thm "Nominal.pt_bij";
+       val pt_perm_compose     = thm "Nominal.pt_perm_compose";
+       val pt_perm_compose'    = thm "Nominal.pt_perm_compose'";
+       val perm_app            = thm "Nominal.pt_fun_app_eq";
+       val at_fresh            = thm "Nominal.at_fresh";
+       val at_calc             = thms "Nominal.at_calc";
+       val at_supp             = thm "Nominal.at_supp";
+       val dj_supp             = thm "Nominal.dj_supp";
+       val fresh_left_ineq     = thm "Nominal.pt_fresh_left_ineq";
+       val fresh_left          = thm "Nominal.pt_fresh_left";
+       val fresh_bij_ineq      = thm "Nominal.pt_fresh_bij_ineq";
+       val fresh_bij           = thm "Nominal.pt_fresh_bij";
+       val pt_pi_rev           = thm "Nominal.pt_pi_rev";
+       val pt_rev_pi           = thm "Nominal.pt_rev_pi";
+       val fresh_fun_eqvt      = thm "Nominal.fresh_fun_equiv";
 
        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
        (* types; this allows for example to use abs_perm (which is a      *)
diff -r d8f252757460 -r 2e909d5309f4 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Fri Apr 28 15:53:47 2006 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Fri Apr 28 15:54:34 2006 +0200
@@ -1,4 +1,9 @@
-(* $Id$ *)
+(*  Title:      HOL/Nominal/nominal_package.ML
+    ID:         $Id$
+    Author:     Stefan Berghofer and Christian Urban, TU Muenchen
+
+Nominal datatype package for Isabelle/HOL.
+*)
 
 signature NOMINAL_PACKAGE =
 sig
@@ -97,10 +102,10 @@
 fun dest_permT (Type ("fun", [Type ("List.list", [Type ("*", [T, _])]),
       Type ("fun", [_, U])])) = (T, U);
 
-fun permTs_of (Const ("nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
+fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
   | permTs_of _ = [];
 
-fun perm_simproc' thy ss (Const ("nominal.perm", T) $ t $ (u as Const ("nominal.perm", U) $ r $ s)) =
+fun perm_simproc' thy ss (Const ("Nominal.perm", T) $ t $ (u as Const ("Nominal.perm", U) $ r $ s)) =
       let
         val (aT as Type (a, []), S) = dest_permT T;
         val (bT as Type (b, []), _) = dest_permT U
@@ -172,8 +177,8 @@
       (Sign.full_name sign n, Sign.full_name sign (n ^ "_Rep"))) dts;
     val rps = map Library.swap ps;
 
-    fun replace_types (Type ("nominal.ABS", [T, U])) = 
-          Type ("fun", [T, Type ("nominal.noption", [replace_types U])])
+    fun replace_types (Type ("Nominal.ABS", [T, U])) = 
+          Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
       | replace_types (Type (s, Ts)) =
           Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
       | replace_types T = T;
@@ -203,7 +208,7 @@
     val perm_types = map (fn (i, _) =>
       let val T = nth_dtyp i
       in permT --> T --> T end) descr;
-    val perm_names = replicate (length new_type_names) "nominal.perm" @
+    val perm_names = replicate (length new_type_names) "Nominal.perm" @
       DatatypeProp.indexify_names (map (fn i => Sign.full_name (sign_of thy1)
         ("perm_" ^ name_of_typ (nth_dtyp i)))
           (length new_type_names upto length descr - 1));
@@ -224,11 +229,11 @@
                 in list_abs (map (pair "x") Us,
                   Const (List.nth (perm_names_types, body_index dt)) $ pi $
                     list_comb (x, map (fn (i, U) =>
-                      Const ("nominal.perm", permT --> U --> U) $
+                      Const ("Nominal.perm", permT --> U --> U) $
                         (Const ("List.rev", permT --> permT) $ pi) $
                         Bound i) ((length Us - 1 downto 0) ~~ Us)))
                 end
-              else Const ("nominal.perm", permT --> T --> T) $ pi $ x
+              else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
             end;  
         in
           (("", HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -261,7 +266,7 @@
             (map (fn (c as (s, T), x) =>
                let val [T1, T2] = binder_types T
                in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
-                 Const ("nominal.perm", T) $ pi $ Free (x, T2))
+                 Const ("Nominal.perm", T) $ pi $ Free (x, T2))
                end)
              (perm_names_types ~~ perm_indnames))))
           (fn _ => EVERY [indtac induction perm_indnames 1,
@@ -345,7 +350,7 @@
           (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a));
       in List.take (map standard (split_conj_thm
         (Goal.prove thy2 [] [] (Logic.mk_implies
-             (HOLogic.mk_Trueprop (Const ("nominal.prm_eq",
+             (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
                 permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
               HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
                 (map (fn ((s, T), x) =>
@@ -402,7 +407,7 @@
                     val pi2 = Free ("pi2", permT2);
                     val perm1 = Const (s, permT1 --> T --> T);
                     val perm2 = Const (s, permT2 --> T --> T);
-                    val perm3 = Const ("nominal.perm", permT1 --> permT2 --> permT2)
+                    val perm3 = Const ("Nominal.perm", permT1 --> permT2 --> permT2)
                   in HOLogic.mk_eq
                     (perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
                      perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
@@ -444,16 +449,16 @@
       (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr));
     val big_rep_name =
       space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
-        (fn (i, ("nominal.noption", _, _)) => NONE
+        (fn (i, ("Nominal.noption", _, _)) => NONE
           | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
     val _ = warning ("big_rep_name: " ^ big_rep_name);
 
     fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
           (case AList.lookup op = descr i of
-             SOME ("nominal.noption", _, [(_, [dt']), _]) =>
+             SOME ("Nominal.noption", _, [(_, [dt']), _]) =>
                apfst (cons dt) (strip_option dt')
            | _ => ([], dtf))
-      | strip_option (DtType ("fun", [dt, DtType ("nominal.noption", [dt'])])) =
+      | strip_option (DtType ("fun", [dt, DtType ("Nominal.noption", [dt'])])) =
           apfst (cons dt) (strip_option dt')
       | strip_option dt = ([], dt);
 
@@ -474,8 +479,8 @@
             val free' = app_bnds free (length Us);
             fun mk_abs_fun (T, (i, t)) =
               let val U = fastype_of t
-              in (i + 1, Const ("nominal.abs_fun", [T, U, T] --->
-                Type ("nominal.noption", [U])) $ mk_Free "y" T i $ t)
+              in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
+                Type ("Nominal.noption", [U])) $ mk_Free "y" T i $ t)
               end
           in (j + 1, j' + length Ts,
             case dt'' of
@@ -496,7 +501,7 @@
 
     val (intr_ts, ind_consts) =
       apfst List.concat (ListPair.unzip (List.mapPartial
-        (fn ((_, ("nominal.noption", _, _)), _) => NONE
+        (fn ((_, ("Nominal.noption", _, _)), _) => NONE
           | ((i, (_, _, constrs)), rep_set_name) =>
               let val T = nth_dtyp i
               in SOME (map (make_intr rep_set_name T) constrs,
@@ -514,7 +519,7 @@
     val _ = warning "proving closure under permutation...";
 
     val perm_indnames' = List.mapPartial
-      (fn (x, (_, ("nominal.noption", _, _))) => NONE | (x, _) => SOME x)
+      (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
       (perm_indnames ~~ descr);
 
     fun mk_perm_closed name = map (fn th => standard (th RS mp))
@@ -527,7 +532,7 @@
                 val T = HOLogic.dest_setT (fastype_of S);
                 val permT = mk_permT (Type (name, []))
               in HOLogic.mk_imp (HOLogic.mk_mem (Free (x, T), S),
-                HOLogic.mk_mem (Const ("nominal.perm", permT --> T --> T) $
+                HOLogic.mk_mem (Const ("Nominal.perm", permT --> T --> T) $
                   Free ("pi", permT) $ Free (x, T), S))
               end) (ind_consts ~~ perm_indnames'))))
         (fn _ => EVERY (* CU: added perm_fun_def in the final tactic in order to deal with funs *)
@@ -561,9 +566,9 @@
           val Const (_, Type (_, [U])) = c
         in apfst (pair r o hd)
           (PureThy.add_defs_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
-            (Const ("nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
+            (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
              Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
-               (Const ("nominal.perm", permT --> U --> U) $ pi $
+               (Const ("Nominal.perm", permT --> U --> U) $ pi $
                  (Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $
                    Free ("x", T))))), [])] thy)
         end))
@@ -637,12 +642,12 @@
         val T = fastype_of x;
         val U = fastype_of t
       in
-        Const ("nominal.abs_fun", T --> U --> T -->
-          Type ("nominal.noption", [U])) $ x $ t
+        Const ("Nominal.abs_fun", T --> U --> T -->
+          Type ("Nominal.noption", [U])) $ x $ t
       end;
 
     val (ty_idxs, _) = foldl
-      (fn ((i, ("nominal.noption", _, _)), p) => p
+      (fn ((i, ("Nominal.noption", _, _)), p) => p
         | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
 
     fun reindex (DtType (s, dts)) = DtType (s, map reindex dts)
@@ -657,7 +662,7 @@
       in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
 
     val (descr'', ndescr) = ListPair.unzip (List.mapPartial
-      (fn (i, ("nominal.noption", _, _)) => NONE
+      (fn (i, ("Nominal.noption", _, _)) => NONE
         | (i, (s, dts, constrs)) =>
              let
                val SOME index = AList.lookup op = ty_idxs i;
@@ -682,7 +687,7 @@
       Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
 
     val recTs' = List.mapPartial
-      (fn ((_, ("nominal.noption", _, _)), T) => NONE
+      (fn ((_, ("Nominal.noption", _, _)), T) => NONE
         | (_, T) => SOME T) (descr ~~ get_rec_types descr sorts');
     val recTs = get_rec_types descr'' sorts';
     val newTs' = Library.take (length new_type_names, recTs');
@@ -783,8 +788,8 @@
         val pi = Free ("pi", permT);
       in
         standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
-            (Const ("nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
-             Rep $ (Const ("nominal.perm", permT --> T --> T) $ pi $ x))))
+            (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
+             Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x))))
           (fn _ => simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @
             perm_closed_thms @ Rep_thms)) 1))
       end) Rep_thms;
@@ -829,7 +834,7 @@
 
           fun perm t =
             let val T = fastype_of t
-            in Const ("nominal.perm", permT --> T --> T) $ pi $ t end;
+            in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
 
           fun constr_arg (dt, (j, l_args, r_args)) =
             let
@@ -949,9 +954,9 @@
           val Ts = map fastype_of args1;
           val c = list_comb (Const (cname, Ts ---> T), args1);
           fun supp t =
-            Const ("nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
+            Const ("Nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
           fun fresh t =
-            Const ("nominal.fresh", atomT --> fastype_of t --> HOLogic.boolT) $
+            Const ("Nominal.fresh", atomT --> fastype_of t --> HOLogic.boolT) $
               Free ("a", atomT) $ t;
           val supp_thm = standard (Goal.prove thy8 [] []
               (HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -1060,7 +1065,7 @@
       in map standard (List.take
         (split_conj_thm (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop
            (foldr1 HOLogic.mk_conj (map (fn (s, T) => HOLogic.mk_mem
-             (Const ("nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T),
+             (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T),
               Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT atomT))))
                (indnames ~~ recTs))))
            (fn _ => indtac dt_induct indnames 1 THEN
@@ -1139,7 +1144,7 @@
 
     val ind_prems = List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
       map (make_ind_prem fsT (fn T => fn t => fn u =>
-        Const ("nominal.fresh", T --> fsT --> HOLogic.boolT) $ t $ u) i T)
+        Const ("Nominal.fresh", T --> fsT --> HOLogic.boolT) $ t $ u) i T)
           (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
     val tnames = DatatypeProp.make_tnames recTs;
     val zs = variantlist (replicate (length descr'') "z", tnames);
@@ -1167,7 +1172,7 @@
       let
         val T = fastype_of1 (Ts, t);
         val U = fastype_of1 (Ts, u)
-      in Const ("nominal.perm", T --> U --> U) $ t $ u end;
+      in Const ("Nominal.perm", T --> U --> U) $ t $ u end;
 
     val aux_ind_vars =
       (DatatypeProp.indexify_names (replicate (length dt_atomTs) "pi") ~~
@@ -1213,7 +1218,7 @@
               (Const ("insert", T --> S --> S) $
                 (foldr (mk_perm (T :: Ts)) (Bound (n - i - j)) prms) $
                 (Const ("op Un", S --> S --> S) $ (f $ Bound (n - k - p)) $
-                   (Const ("nominal.supp", U --> S) $
+                   (Const ("Nominal.supp", U --> S) $
                      foldr (mk_perm (T :: Ts)) (Bound (n - i')) prms))))))
       end;
 
@@ -1304,7 +1309,7 @@
       map (fn (_, f) =>
         let val f' = Logic.varify f
         in (cterm_of thy9 f',
-          cterm_of thy9 (Const ("nominal.supp", fastype_of f')))
+          cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
         end) fresh_fs) induct_aux;
 
     val induct = standard (Goal.prove thy9 [] ind_prems ind_concl
@@ -1352,7 +1357,7 @@
     fun partition_cargs idxs xs = map (fn (i, j) =>
       (List.take (List.drop (xs, i), j), List.nth (xs, i + j))) idxs;
 
-    fun mk_fresh_fun (a, t) = Const ("nominal.fresh_fun",
+    fun mk_fresh_fun (a, t) = Const ("Nominal.fresh_fun",
       (fastype_of a --> fastype_of t) --> fastype_of t) $ lambda a t;
 
     fun make_rec_intr T rec_set ((rec_intr_ts, l), ((cname, cargs), idxs)) =
diff -r d8f252757460 -r 2e909d5309f4 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Fri Apr 28 15:53:47 2006 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Fri Apr 28 15:54:34 2006 +0200
@@ -1,7 +1,10 @@
-(* $Id$ *)
+(*  Title:      HOL/Nominal/nominal_permeq.ML
+    ID:         $Id$
+    Author:     Christian Urban, TU Muenchen
 
-(* METHODS FOR SIMPLIFYING PERMUTATIONS AND     *)
-(* FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
+Methods for simplifying permutations and
+for analysing equations involving permutations.
+*)
 
 local
 
@@ -10,8 +13,8 @@
 fun dynamic_thm ss name = ProofContext.get_thm (Simplifier.the_context ss) (Name name);
 
 (* a tactic simplyfying permutations *)
-val perm_fun_def = thm "nominal.perm_fun_def"
-val perm_eq_app = thm "nominal.pt_fun_app_eq"
+val perm_fun_def = thm "Nominal.perm_fun_def"
+val perm_eq_app = thm "Nominal.pt_fun_app_eq"
 
 fun perm_eval_tac ss i =
     let
@@ -22,7 +25,7 @@
            (* more arguments                                                  *)
            fun applicable t = 
 	       (case (strip_comb t) of
-		  (Const ("nominal.perm",_),ts) => (length ts) >= 2
+		  (Const ("Nominal.perm",_),ts) => (length ts) >= 2
 		| (Const _,_) => false
 		| _ => true)
 
@@ -30,7 +33,7 @@
         (case redex of 
         (* case pi o (f x) == (pi o f) (pi o x)          *)
         (* special treatment according to the head of f  *)
-        (Const("nominal.perm",
+        (Const("Nominal.perm",
           Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
 	   (case (applicable f) of
                 false => NONE  
@@ -42,14 +45,14 @@
 		in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end)
 
         (* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
-        | (Const("nominal.perm",_) $ pi $ (Abs _)) => SOME (perm_fun_def)
+        | (Const("Nominal.perm",_) $ pi $ (Abs _)) => SOME (perm_fun_def)
 
         (* no redex otherwise *) 
         | _ => NONE) end
 
 	val perm_eval =
 	    Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval" 
-	    ["nominal.perm pi x"] perm_eval_simproc;
+	    ["Nominal.perm pi x"] perm_eval_simproc;
 
       (* these lemmas are created dynamically according to the atom types *) 
       val perm_swap        = dynamic_thms ss "perm_swap"
@@ -80,8 +83,8 @@
     let
 	fun perm_compose_simproc sg ss redex =
 	(case redex of
-           (Const ("nominal.perm", Type ("fun", [Type ("List.list", 
-             [Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("nominal.perm", 
+           (Const ("Nominal.perm", Type ("fun", [Type ("List.list", 
+             [Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
                Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ 
                 pi2 $ t)) =>
         let
@@ -107,7 +110,7 @@
 	  
       val perm_compose  =
 	Simplifier.simproc (the_context()) "perm_compose" 
-	["nominal.perm pi1 (nominal.perm pi2 t)"] perm_compose_simproc;
+	["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc;
 
       val ss' = Simplifier.theory_context (the_context ()) empty_ss	  
 
@@ -133,7 +136,7 @@
 (*   %x. pi o (f ((rev pi) o x)) = rhs        *)
 fun unfold_perm_fun_def_tac i = 
     let
-	val perm_fun_def = thm "nominal.perm_fun_def"
+	val perm_fun_def = thm "Nominal.perm_fun_def"
     in
 	("unfolding of permutations on functions", 
          rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i)
@@ -148,7 +151,7 @@
 (* should be able to analyse pi o fresh_fun () = fresh_fun instances *) 
 fun fresh_fun_eqvt_tac i =
     let
-	val fresh_fun_equiv = thm "nominal.fresh_fun_equiv_ineq"
+	val fresh_fun_equiv = thm "Nominal.fresh_fun_equiv_ineq"
     in
 	("fresh_fun equivariance", rtac (fresh_fun_equiv RS trans) i)
     end		       
@@ -184,9 +187,9 @@
 (* and strips off the intros, then applies perm_full_simp_tac *)
 fun supports_tac tactical ss i =
   let 
-      val supports_def = thm "nominal.op supports_def";
-      val fresh_def    = thm "nominal.fresh_def";
-      val fresh_prod   = thm "nominal.fresh_prod";
+      val supports_def = thm "Nominal.op supports_def";
+      val fresh_def    = thm "Nominal.fresh_def";
+      val fresh_prod   = thm "Nominal.fresh_prod";
       val simps        = [supports_def,symmetric fresh_def,fresh_prod]
   in
       EVERY [tactical ("unfolding of supports   ", simp_tac (HOL_basic_ss addsimps simps) i),
@@ -215,7 +218,7 @@
     let val goal = List.nth(cprems_of st, i-1)
     in
       case Logic.strip_assums_concl (term_of goal) of
-          _ $ (Const ("op :", _) $ (Const ("nominal.supp", T) $ x) $
+          _ $ (Const ("op :", _) $ (Const ("Nominal.supp", T) $ x) $
             Const ("Finite_Set.Finites", _)) =>
           let
             val cert = Thm.cterm_of (sign_of_thm st);
@@ -226,7 +229,7 @@
                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
               HOLogic.unit vs;
             val s' = list_abs (ps,
-              Const ("nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
+              Const ("Nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
             val supports_rule' = Thm.lift_rule goal supports_rule;
             val _ $ (_ $ S $ _) =
               Logic.strip_assums_concl (hd (prems_of supports_rule'));