Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Fri, 17 Jan 2025 10:56:10 +0100
changeset 81839 ea0c7189b15b
parent 81838 834024a7863d
child 81840 345e592792fd
tuned;
src/HOL/Import/import_rule.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Import/import_rule.ML	Fri Jan 17 10:53:30 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Fri Jan 17 10:56:10 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 (make_name c)))
+      | NONE => Sign.full_bname thy (make_name c))
   in Type (d, args) end
 
 fun make_const thy (c, ty) =
@@ -310,7 +310,7 @@
     val d =
       (case Import_Data.get_const_map thy c of
         SOME d => d
-      | NONE => Sign.full_name thy (Binding.name (make_name c)))
+      | NONE => Sign.full_bname thy (make_name c))
   in Const (d, ty) end
 
 fun get (map, no) s =
isabelle