# HG changeset patch
# User wenzelm
# Date 1729593680 -7200
# Node ID ed326e93b835aeabc8c850dc0db52be7b1de723e
# Parent  2f5c1761541dbbf357d0480e49ecc3bc2f5550ed
misc tuning and clarification;

diff -r 2f5c1761541d -r ed326e93b835 src/HOL/HOLCF/Tools/cont_consts.ML
--- a/src/HOL/HOLCF/Tools/cont_consts.ML	Tue Oct 22 12:28:32 2024 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Tue Oct 22 12:41:20 2024 +0200
@@ -16,44 +16,19 @@
 structure Cont_Consts: CONT_CONSTS =
 struct
 
-(* type cfun *)
-
 fun count_cfun \<^Type>\<open>cfun _ B\<close> = count_cfun B + 1
   | count_cfun _ = 0
 
 fun change_cfun 0 T = T
   | change_cfun n \<^Type>\<open>cfun A B\<close> = \<^Type>\<open>fun A \<open>change_cfun (n - 1) B\<close>\<close>
-  | change_cfun _ T = raise TYPE ("cont_consts: change_arrow", [T], [])
-
-
-(* translations *)
-
-fun trans_rules c1 c2 n mx =
-  let
-    val xs = Name.invent Name.context "xa" n
-    val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant c1, Ast.Constant c2)
-  in
-    [Syntax.Parse_Print_Rule
-      (Ast.mk_appl (Ast.Constant c1) (map Ast.Variable xs),
-        fold (fn x => fn t =>
-            Ast.mk_appl (Ast.Constant \<^const_syntax>\<open>Rep_cfun\<close>) [t, Ast.Variable x])
-          xs (Ast.Constant c2))] @
-    (case mx of
-      Infix _ => [extra_parse_rule]
-    | Infixl _ => [extra_parse_rule]
-    | Infixr _ => [extra_parse_rule]
-    | _ => [])
-  end
-
-
-(* add_consts *)
+  | change_cfun _ T = raise TYPE ("cont_consts: change_cfun", [T], [])
 
 fun gen_add_consts prep_typ raw_decls thy =
   let
     val thy_ctxt = Proof_Context.init_global thy
 
     fun is_cont_const (_, _, NoSyn) = false
-      | is_cont_const (_, _, Binder _) = false    (* FIXME ? *)
+      | is_cont_const (_, _, Binder _) = false
       | is_cont_const (b, T, mx) =
           let
             val n = Mixfix.mixfix_args thy_ctxt mx handle ERROR msg =>
@@ -65,8 +40,15 @@
         val c = Sign.full_name thy b
         val c1 = Lexicon.mark_syntax c
         val c2 = Lexicon.mark_const c
-        val n = Mixfix.mixfix_args thy_ctxt mx
-      in ((b, T, NoSyn), (c1, change_cfun n T, mx), trans_rules c1 c2 n mx) end
+        val xs = Name.invent Name.context "xa" (Mixfix.mixfix_args thy_ctxt mx)
+        val trans_rules =
+          Syntax.Parse_Print_Rule
+            (Ast.mk_appl (Ast.Constant c1) (map Ast.Variable xs),
+              fold (fn x => fn t =>
+                  Ast.mk_appl (Ast.Constant \<^const_syntax>\<open>Rep_cfun\<close>) [t, Ast.Variable x])
+                xs (Ast.Constant c2)) ::
+          (if Mixfix.is_infix mx then [Syntax.Parse_Rule (Ast.Constant c1, Ast.Constant c2)] else [])
+      in ((b, T, NoSyn), (c1, change_cfun (length xs) T, mx), trans_rules) end
 
     val decls = map (fn (b, T, mx) => (b, prep_typ thy T, mx)) raw_decls
     val (cont_decls, normal_decls) = List.partition is_cont_const decls
diff -r 2f5c1761541d -r ed326e93b835 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Tue Oct 22 12:28:32 2024 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Tue Oct 22 12:41:20 2024 +0200
@@ -21,6 +21,7 @@
   include BASIC_MIXFIX
   val mixfix: string -> mixfix
   val is_empty: mixfix -> bool
+  val is_infix: mixfix -> bool
   val equal: mixfix * mixfix -> bool
   val range_of: mixfix -> Position.range
   val pos_of: mixfix -> Position.T
@@ -54,6 +55,11 @@
 fun is_empty NoSyn = true
   | is_empty _ = false;
 
+fun is_infix (Infix _) = true
+  | is_infix (Infixl _) = true
+  | is_infix (Infixr _) = true
+  | is_infix _ = false;
+
 fun equal (NoSyn, NoSyn) = true
   | equal (Mixfix (sy, ps, p, _), Mixfix (sy', ps', p', _)) =
       Input.equal_content (sy, sy') andalso ps = ps' andalso p = p'