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-General/nominal_atoms.ML
changeset 2396 f2f611daf480
parent 2168 ce0255ffaeb4
child 2467 67b3933c3190 
--- a/Nominal-General/nominal_atoms.ML	Wed Aug 11 19:53:57 2010 +0800
+++ b/Nominal-General/nominal_atoms.ML	Thu Aug 12 21:29:35 2010 +0800
@@ -53,7 +53,7 @@
 
     (* at class instance *)
     val lthy =
-      Theory_Target.instantiation ([full_tname], [], @{sort at}) thy;
+      Class.instantiation ([full_tname], [], @{sort at}) thy;
     val ((_, (_, permute_ldef)), lthy) =
       Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy;
     val ((_, (_, atom_ldef)), lthy) =
nominal2