src/HOL/Tools/Datatype/datatype_case.ML

 
 fun strip_constraints (Const (@{syntax_const "_constrain"}, _) $ t $ tT) =
       strip_constraints t ||> cons tT
   | strip_constraints t = (t, []);
 
-val recover_constraints =
-  fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT);
-
+fun constrain tT t = Syntax.const @{syntax_const "_constrain"} $ t $ tT;
 fun constrain_Abs tT t = Syntax.const @{syntax_const "_constrainAbs"} $ t $ tT;
 
 
 (*Produce an instance of a constructor, plus fresh variables for its arguments.*)
 fun fresh_constr ty_match ty_inst colty used c =

   in (c', gvars) end;
 
 fun strip_comb_positions tm =
   let
     fun result t ts = (Term_Position.strip_positions t, ts);
-    fun strip (t as (Const (@{syntax_const "_constrain"}, _) $ _ $ _)) ts = result t ts
+    fun strip (t as Const (@{syntax_const "_constrain"}, _) $ _ $ _) ts = result t ts
       | strip (f $ t) ts = strip f (t :: ts)
       | strip t ts = result t ts;
   in strip tm [] end;
 
 (*Go through a list of rows and pick out the ones beginning with a

               if length args = k then
                 let val (args', cnstrts') = split_list (map strip_constraints args) in
                   ((((prfx, args' @ ps), rhs) :: in_group, not_in_group),
                    (default_names names args', map2 append cnstrts cnstrts'))
                 end
-              else raise CASE_ERROR ("Wrong number of arguments for constructor " ^ name, i)
+              else raise CASE_ERROR ("Wrong number of arguments for constructor " ^ quote name, i)
             else ((in_group, row :: not_in_group), (names, cnstrts))
         | _ => raise CASE_ERROR ("Not a constructor pattern", i)))
     rows (([], []), (replicate k "", replicate k [])) |>> pairself rev
   end;
 

                           (replicate (length ps) "x");
                     in
                       [((prfx, gvars @ map Free (xs ~~ Ts)),
                         (Const (@{const_syntax undefined}, res_ty), ~1))]
                     end
-                  else in_group
+                  else in_group;
               in
                 {constructor = c',
                  new_formals = gvars,
                  names = names,
                  constraints = cnstrts,

 
 fun mk_case ctxt ty_match ty_inst type_of used range_ty =
   let
     val get_info = Datatype_Data.info_of_constr_permissive (Proof_Context.theory_of ctxt);
 
-    fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand_var_row", ~1)
+    fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand", ~1)
       | expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
           if is_Free p then
             let
               val used' = add_row_used row used;
               fun expnd c =

                   val rows' = map (fn ((v, _), row) => row ||>
                     apfst (subst_free [(v, u)]) |>> v_to_prfx) (col0 ~~ rows);
                 in mk us rows' end
             | SOME (Const (cname, cT), i) =>
                 (case Option.map ty_info (get_info (cname, cT)) of
-                  NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ cname, i)
+                  NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ quote cname, i)
                 | SOME {case_name, constructors} =>
                     let
                       val pty = body_type cT;
                       val used' = fold Term.add_free_names us used;
                       val nrows = maps (expand constructors used' pty) rows;

 
         val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
       in
         make_case_untyped ctxt
           (if err then Error else Warning) []
-          (recover_constraints (filter_out Term_Position.is_position (flat cnstrts)) t)
+          (fold constrain (filter_out Term_Position.is_position (flat cnstrts)) t)
           cases
       end
   | case_tr _ _ _ = case_error "case_tr";
 
 val trfun_setup =