Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_atoms.ML
changeset 3045 d0ad264f8c4f
parent 2891 304dfe6cc83a
child 3135 92b9b8d2888d 
--- a/Nominal/nominal_atoms.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_atoms.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -62,9 +62,9 @@
       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_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 ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy);
+    val permute_def = singleton (Proof_Context.export lthy ctxt_thy) permute_ldef;
+    val atom_def = singleton (Proof_Context.export lthy ctxt_thy) atom_ldef;
     val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def];
     val sort_thm = @{thm at_class_sort} OF [type_definition, atom_def]
     val thy = lthy
nominal2