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