--- 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 *}