# HG changeset patch
# User urbanc
# Date 1177112055 -7200
# Node ID f28f627546447ce9316c54d238d9eddf76880f05
# Parent  c2e9705f804ec67eb1bbe5ba4a1a2c97d3b558ef
tuned the setup of fresh_fun

diff -r c2e9705f804e -r f28f62754644 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Fri Apr 20 17:58:27 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Sat Apr 21 01:34:15 2007 +0200
@@ -8,6 +8,7 @@
   ("nominal_package.ML")
   ("nominal_induct.ML") 
   ("nominal_permeq.ML")
+  ("nominal_fresh_fun.ML")
   ("nominal_primrec.ML")
   ("nominal_inductive.ML")
 begin 
@@ -3204,10 +3205,6 @@
 (* various tactics for analysing permutations, supports etc *)
 use "nominal_permeq.ML";
 
-(****************************************************************)
-(* tactics for generating fresh names and simplifying fresh_fun *)
-use "nominal_fresh_fun.ML";
-
 method_setup perm_simp =
   {* NominalPermeq.perm_simp_meth *}
   {* simp rules and simprocs for analysing permutations *}
@@ -3248,6 +3245,9 @@
   {* NominalPermeq.fresh_guess_meth_debug *}
   {* tactic for deciding whether an atom is fresh for something including debugging facilities *}
 
+(*****************************************************************)
+(* tactics for generating fresh names and simplifying fresh_funs *)
+use "nominal_fresh_fun.ML";
 
 method_setup generate_fresh = 
   {* setup_generate_fresh *}