diff -r a2d18fea844a -r e95831757903 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Tue Nov 12 14:00:56 2013 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Tue Nov 12 14:24:34 2013 +0100
@@ -37,12 +37,17 @@
       let
         val (hd, args) = strip_comb t
       in
-        (((case Datatype.info_of_constr thy (dest_Const hd) of
-             SOME _ => ()
-           | NONE => err "Non-constructor pattern")
-          handle TERM ("dest_Const", _) => err "Non-constructor patterns");
-         map check_constr_pattern args;
-         ())
+        (case hd of
+          Const (hd_s, hd_T) =>
+          (case body_type hd_T of
+            Type (Tname, _) =>
+            (case Ctr_Sugar.ctr_sugar_of ctxt Tname of
+              SOME {ctrs, ...} => exists (fn Const (s, _) => s = hd_s) ctrs
+            | NONE => false)
+          | _ => false)
+        | _ => false) orelse err "Non-constructor pattern";
+        map check_constr_pattern args;
+        ()
       end
 
     val (_, qs, gs, args, _) = split_def ctxt (K true) geq