src/HOL/Tools/Function/fun.ML
changeset 54407 e95831757903
parent 49965 ee25a04fa06a
child 56254 a2dd9200854d
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Tue Nov 12 14:00:56 2013 +0100
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Tue Nov 12 14:24:34 2013 +0100
     1.3 @@ -37,12 +37,17 @@
     1.4        let
     1.5          val (hd, args) = strip_comb t
     1.6        in
     1.7 -        (((case Datatype.info_of_constr thy (dest_Const hd) of
     1.8 -             SOME _ => ()
     1.9 -           | NONE => err "Non-constructor pattern")
    1.10 -          handle TERM ("dest_Const", _) => err "Non-constructor patterns");
    1.11 -         map check_constr_pattern args;
    1.12 -         ())
    1.13 +        (case hd of
    1.14 +          Const (hd_s, hd_T) =>
    1.15 +          (case body_type hd_T of
    1.16 +            Type (Tname, _) =>
    1.17 +            (case Ctr_Sugar.ctr_sugar_of ctxt Tname of
    1.18 +              SOME {ctrs, ...} => exists (fn Const (s, _) => s = hd_s) ctrs
    1.19 +            | NONE => false)
    1.20 +          | _ => false)
    1.21 +        | _ => false) orelse err "Non-constructor pattern";
    1.22 +        map check_constr_pattern args;
    1.23 +        ()
    1.24        end
    1.25  
    1.26      val (_, qs, gs, args, _) = split_def ctxt (K true) geq