--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sun Aug 04 17:39:47 2024 +0200
@@ -446,8 +446,8 @@
(* define syntax for case combinator *)
(* TODO: re-implement case syntax using a parse translation *)
local
- fun syntax c = Lexicon.mark_const (fst (dest_Const c))
- fun xconst c = Long_Name.base_name (fst (dest_Const c))
+ fun syntax c = Lexicon.mark_const (dest_Const_name c)
+ fun xconst c = Long_Name.base_name (dest_Const_name c)
fun c_ast authentic con = Ast.Constant (if authentic then syntax con else xconst con)
fun showint n = string_of_int (n+1)
fun expvar n = Ast.Variable ("e" ^ showint n)
@@ -803,8 +803,8 @@
(* register match combinators with fixrec package *)
local
- val con_names = map (fst o dest_Const o fst) spec
- val mat_names = map (fst o dest_Const) match_consts
+ val con_names = map (dest_Const_name o fst) spec
+ val mat_names = map dest_Const_name match_consts
in
val thy = Fixrec.add_matchers (con_names ~~ mat_names) thy
end