# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272983431 -7200
# Node ID 13da6048711210ee547229fcfe5832af2f9c00c1
# Parent  495b6feb76a8f67d4da890abd6d94206a5157638
Fix for new isabelle

diff -r 495b6feb76a8 -r 13da60487112 Nominal-General/nominal_atoms.ML
--- 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];