src/HOL/Nominal/nominal_permeq.ML

   val fresh_gs_meth_debug : Method.src -> Proof.context -> Proof.method
 end
 
 structure NominalPermeq : NOMINAL_PERMEQ =
 struct
+
+val Finites_emptyI = thm "Finites.emptyI";
+val finite_Un = thm "finite_Un";
 
 (* pulls out dynamically a thm via the proof state *)
 fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) (Name name);
 fun dynamic_thm st name = PureThy.get_thm (theory_of_thm st) (Name name);
 

             val supports_rule' = Thm.lift_rule goal supports_rule;
             val _ $ (_ $ S $ _) =
               Logic.strip_assums_concl (hd (prems_of supports_rule'));
             val supports_rule'' = Drule.cterm_instantiate
               [(cert (head_of S), cert s')] supports_rule'
-            val ss' = ss addsimps [supp_prod, supp_unit, finite_Un, Finites.emptyI]
+            val ss' = ss addsimps [supp_prod, supp_unit, finite_Un, Finites_emptyI]
           in
             (tactical ("guessing of the right supports-set",
                       EVERY [compose_tac (false, supports_rule'', 2) i,
                              asm_full_simp_tac ss' (i+1),
                              supports_tac tactical ss i])) st

             val _ $ (_ $ S $ _) =
               Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
             val supports_fresh_rule'' = Drule.cterm_instantiate
               [(cert (head_of S), cert s')] supports_fresh_rule'
 	    val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit]
-            val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,Finites.emptyI]
+            val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,Finites_emptyI]
             (* FIXME sometimes these rewrite rules are already in the ss, *)
             (* which produces a warning                                   *)
           in
             (tactical ("guessing of the right set that supports the goal",
                       EVERY [compose_tac (false, supports_fresh_rule'', 3) i,