Mercurial Mercurial > repos > isabelle / 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.
src/HOL/Nominal/nominal_thmdecls.ML
changeset 30280 eb98b49ef835
parent 30088 fe6eac03b816
child 30364 577edc39b501 
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -115,7 +115,7 @@
                (Var (n,ty))) =>
              let
                 (* FIXME: this should be an operation the library *)
-                val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
+                val class_name = (NameSpace.map_base_name (fn s => "pt_"^s) tyatm)
              in
                 if (Sign.of_sort thy (ty,[class_name]))
                 then [(pi,typi)]
isabelle