Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merge
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 04 May 2010 16:33:30 +0200
changeset 2054 f2f427bc4fd1
parent 2050 8bd75f2fd7b0 (current diff)
parent 2051 13da60487112 (diff)
child 2055 5a8a3e209b95
merge
--- 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];
nominal2