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/Import/import_rule.ML
changeset 81838 834024a7863d
parent 81837 cc24add5b738
child 81839 ea0c7189b15b 
--- a/src/HOL/Import/import_rule.ML	Fri Jan 17 10:51:47 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Fri Jan 17 10:53:30 2025 +0100
@@ -302,7 +302,7 @@
     val d =
       (case Import_Data.get_typ_map thy c of
         SOME d => d
-      | NONE => Sign.full_name thy (Binding.name c))
+      | NONE => Sign.full_name thy (Binding.name (make_name c)))
   in Type (d, args) end
 
 fun make_const thy (c, ty) =
isabelle