--- a/Nominal/Atoms.thy	Mon May 09 04:49:58 2011 +0100
+++ b/Nominal/Atoms.thy	Tue May 10 07:47:06 2011 +0100
@@ -225,10 +225,12 @@
 
 declare [[coercion "atom::var2\<Rightarrow>atom"]]
 
+(*
 lemma
   fixes a::"var1" and b::"var2"
   shows "a \<sharp> t \<and> b \<sharp> t"
 oops
+*)
 
 (* does not yet work: it needs image as
    coercion map *)

--- a/Nominal/Ex/Datatypes.thy	Mon May 09 04:49:58 2011 +0100
+++ b/Nominal/Ex/Datatypes.thy	Tue May 10 07:47:06 2011 +0100
@@ -91,6 +91,8 @@
 thm set_ty.size_eqvt
 thm set_ty.supp
 
+
+
 end
 
 

--- a/Nominal/Nominal2.thy	Mon May 09 04:49:58 2011 +0100
+++ b/Nominal/Nominal2.thy	Tue May 10 07:47:06 2011 +0100
@@ -323,19 +323,19 @@
 
   val _ = trace_msg (K "Defining the quotient constants...")
   val qconstrs_descrs =
-    (map2 o map2) (fn (b, _, mx) => fn t => (Variable.name b, t, mx)) (get_cnstrs dts) raw_constrs
+    (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) (get_cnstrs dts) raw_constrs
 
   val qbns_descr =
-    map2 (fn (b, _, mx) => fn t => (Variable.name b, t, mx)) bn_funs raw_bns
+    map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) bn_funs raw_bns
 
   val qfvs_descr = 
     map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs
 
   val qfv_bns_descr = 
-    map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.name b, t, NoSyn)) bn_funs raw_fv_bns
+    map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_fv_bns
 
   val qalpha_bns_descr = 
-    map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.name b, t, NoSyn)) bn_funs  alpha_bn_trms
+    map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn)) bn_funs  alpha_bn_trms
 
   val qperm_descr =
     map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs
@@ -344,7 +344,7 @@
     map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms
 
   val qperm_bn_descr = 
-    map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.name b, t, NoSyn)) bn_funs raw_perm_bns
+    map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_perm_bns
      
   val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), 
     lthy8) = 

--- a/Nominal/Nominal2_Base.thy	Mon May 09 04:49:58 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue May 10 07:47:06 2011 +0100
@@ -743,7 +743,6 @@
 text {* provides perm_simp methods *}
 
 use "nominal_permeq.ML"
-setup Nominal_Permeq.setup
 
 method_setup perm_simp =
  {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}

--- a/Nominal/nominal_function_core.ML	Mon May 09 04:49:58 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Tue May 10 07:47:06 2011 +0100
@@ -540,10 +540,10 @@
     fun requantify orig_intro thm =
       let
         val (qs, t) = dest_all_all orig_intro
-        val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T)
-        val vars = Term.add_vars (prop_of thm) [] |> rev
+        val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T)
+        val vars = Term.add_vars (prop_of thm) []
         val varmap = AList.lookup (op =) (frees ~~ map fst vars)
-          #> the_default ("",0)
+           #> the_default ("",0)
       in
         fold_rev (fn Free (n, T) =>
           forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm

--- a/Nominal/nominal_induct.ML	Mon May 09 04:49:58 2011 +0100
+++ b/Nominal/nominal_induct.ML	Tue May 10 07:47:06 2011 +0100
@@ -95,7 +95,7 @@
     val finish_rule =
       split_all_tuples
       #> rename_params_rule true
-        (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding);
+        (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding);
 
     fun rule_cases ctxt r =
       let val r' = if simp then Induct.simplified_rule ctxt r else r

--- a/Nominal/nominal_mutual.ML	Mon May 09 04:49:58 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Tue May 10 07:47:06 2011 +0100
@@ -118,10 +118,11 @@
     fun convert_eqs (f, qs, gs, args, rhs) =
       let
         val MutualPart {i, i', ...} = get_part f parts
+        val rhs' = rhs
+             |> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n) | t => t)
       in
         (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
-         SumTree.mk_inj RST n' i' (replace_frees rews rhs)
-         |> Envir.beta_norm)
+         Envir.beta_norm (SumTree.mk_inj RST n' i' rhs'))
       end
 
     val qglrs = map convert_eqs fqgars

--- a/Nominal/nominal_permeq.ML	Mon May 09 04:49:58 2011 +0100
+++ b/Nominal/nominal_permeq.ML	Tue May 10 07:47:06 2011 +0100
@@ -26,7 +26,6 @@
   val args_parser: (thm list * string list) context_parser
 
   val trace_eqvt: bool Config.T
-  val setup: theory -> theory
 end;
 
 (* 
@@ -95,7 +94,7 @@
 
 
 (* tracing infrastructure *)
-val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false);
+val trace_eqvt = Attrib.setup_config_bool @{binding "trace_eqvt"} (K false);
 
 fun trace_enabled ctxt = Config.get ctxt trace_eqvt
 
@@ -211,10 +210,6 @@
 fun eqvt_tac ctxt config = 
   CONVERSION (eqvt_conv ctxt config)
 
-(* setup of the configuration value *)
-val setup =
-  trace_eqvt_setup
-
 
 (** methods **)
 fun unless_more_args scan = Scan.unless (Scan.lift ((Args.$$$ "exclude") -- Args.colon)) scan