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 2467 67b3933c3190
parent 2396 f2f611daf480 
--- a/Nominal-General/nominal_atoms.ML	Sat Sep 04 05:43:03 2010 +0800
+++ b/Nominal-General/nominal_atoms.ML	Sat Sep 04 06:10:04 2010 +0800
@@ -26,7 +26,7 @@
 
 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
   let
-    val _ = Theory.requires thy "Nominal2_Atoms" "nominal logic";
+    val _ = Theory.requires thy "Nominal2_Base" "nominal logic";
     val str = Sign.full_name thy name;
 
     (* typedef *)
nominal2