--- a/Nominal-General/nominal_atoms.ML	Tue May 04 12:34:33 2010 +0200
+++ b/Nominal-General/nominal_atoms.ML	Tue May 04 16:30:31 2010 +0200
@@ -58,7 +58,7 @@
       Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy;
     val ((_, (_, atom_ldef)), lthy) =
       Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy;
-    val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
+    val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
     val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef;
     val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef;
     val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def];