src/HOL/Tools/Datatype/datatype_case.ML
changeset 46188 8297006abc13
parent 46140 463b594e186a
child 46219 426ed18eba43
equal deleted inserted replaced
46187:f009e0fe8643 46188:8297006abc13
    61 
    61 
    62 fun default_name name (t, cs) =
    62 fun default_name name (t, cs) =
    63   let
    63   let
    64     val name' = if name = "" then (case t of Free (name', _) => name' | _ => name) else name;
    64     val name' = if name = "" then (case t of Free (name', _) => name' | _ => name) else name;
    65     val cs' = if is_Free t then cs else filter_out Term_Position.is_position cs;
    65     val cs' = if is_Free t then cs else filter_out Term_Position.is_position cs;
    66   in (name, cs') end;
    66   in (name', cs') end;
    67 
    67 
    68 fun strip_constraints (Const (@{syntax_const "_constrain"}, _) $ t $ tT) =
    68 fun strip_constraints (Const (@{syntax_const "_constrain"}, _) $ t $ tT) =
    69       strip_constraints t ||> cons tT
    69       strip_constraints t ||> cons tT
    70   | strip_constraints t = (t, []);
    70   | strip_constraints t = (t, []);
    71 
    71