src/Tools/Code/code_printer.ML

     -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
   val gen_pr_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list)
     -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> (string -> const_syntax option)
     -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
-  val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
+  val gen_pr_bind: (Pretty.T option * itype -> Pretty.T)
     -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm -> fixity
-    -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
+    -> iterm option * itype -> var_ctxt -> Pretty.T * var_ctxt
 
   val mk_name_module: Name.context -> string option -> (string -> string option)
     -> 'a Graph.T -> string -> string
   val dest_name: string -> string * string
 end;

           then case chop k ts of (ts1, ts2) =>
             brackify fxy (pr' APP ts1 :: map (pr_term thm vars BR) ts2)
           else pr_term thm vars fxy (Code_Thingol.eta_expand k app)
         end;
 
-fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
-  let
-    val vs = case pat
+fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) (some_pat, ty : itype) vars =
+  let
+    val vs = case some_pat
      of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
       | NONE => [];
-    val vars' = intro_vars (the_list v) vars;
-    val vars'' = intro_vars vs vars';
-    val v' = Option.map (lookup_var vars') v;
-    val pat' = Option.map (pr_term thm vars'' fxy) pat;
-  in (pr_bind ((v', pat'), ty), vars'') end;
+    val vars' = intro_vars vs vars;
+    val some_pat' = Option.map (pr_term thm vars' fxy) some_pat;
+  in (pr_bind (some_pat', ty), vars') end;
 
 
 (* mixfix syntax *)
 
 datatype 'a mixfix =