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:46:59 +0100
changeset 81836 e6836cc115b9
parent 81835 35abb6dd8bd2
child 81837 cc24add5b738
tuned;
src/HOL/Import/import_data.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Import/import_data.ML	Fri Jan 17 10:43:23 2025 +0100
+++ b/src/HOL/Import/import_data.ML	Fri Jan 17 10:46:59 2025 +0100
@@ -53,7 +53,7 @@
 fun add_const_map_cmd s1 raw_s2 thy =
   let
     val ctxt = Proof_Context.init_global thy
-    val Const (s2, _) = Proof_Context.read_const {proper = true, strict = false} ctxt raw_s2
+    val s2 = dest_Const_name (Proof_Context.read_const {proper = true, strict = false} ctxt raw_s2)
   in add_const_map s1 s2 thy end
 
 fun add_typ_map s1 s2 thy =
@@ -64,7 +64,7 @@
 fun add_typ_map_cmd s1 raw_s2 thy =
   let
     val ctxt = Proof_Context.init_global thy
-    val Type (s2, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt raw_s2
+    val s2 = dest_Type_name (Proof_Context.read_type_name {proper = true, strict = false} ctxt raw_s2)
   in add_typ_map s1 s2 thy end
 
 fun add_const_def s th name_opt thy =
isabelle