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.
Fix for new isabelle
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 04 May 2010 16:30:31 +0200
changeset 2051 13da60487112
parent 2042 495b6feb76a8
child 2054 f2f427bc4fd1
Fix for new isabelle
Nominal-General/nominal_atoms.ML file | annotate | diff | comparison | revisions 
--- 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];
nominal2