# HG changeset patch
# User wenzelm
# Date 1389445953 -3600
# Node ID 8dc8d427b3138246c8b1ea82c0736c182e44c6a5
# Parent  fe454ca3405f43678cc9f1720dc7cc6e12ac6020
tuned signature;

diff -r fe454ca3405f -r 8dc8d427b313 src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Fri Jan 10 23:44:03 2014 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Sat Jan 11 14:12:33 2014 +0100
@@ -12,6 +12,7 @@
 
 signature NOMINAL_THMDECLS =
 sig
+  val nominal_eqvt_debug: bool Config.T
   val eqvt_add: attribute
   val eqvt_del: attribute
   val eqvt_force_add: attribute
@@ -69,7 +70,6 @@
 
 fun get_derived_thm ctxt hyp concl orig_thm pi typi =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val pi' = Var (pi, typi);
     val lhs = Const (@{const_name "perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
     val ([goal_term, pi''], ctxt') = Variable.import_terms false