# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272983610 -7200
# Node ID f2f427bc4fd171e58ed0d3e3a63a6c02d8fd06c8
# Parent  8bd75f2fd7b0f6856f55d4286f1d117e2684a777# Parent  13da6048711210ee547229fcfe5832af2f9c00c1
merge

diff -r 8bd75f2fd7b0 -r f2f427bc4fd1 Nominal-General/nominal_atoms.ML
--- a/Nominal-General/nominal_atoms.ML	Tue May 04 16:18:07 2010 +0200
+++ b/Nominal-General/nominal_atoms.ML	Tue May 04 16:33:30 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];