src/HOL/Tools/Datatype/datatype_data.ML

   val the_spec : theory -> string -> (string * sort) list * (string * typ list) list
   val all_distincts : theory -> typ list -> thm list list
   val get_constrs : theory -> string -> (string * typ) list option
   val get_all : theory -> info Symtab.table
   val info_of_constr : theory -> string * typ -> info option
+  val info_of_constr_permissive : theory -> string * typ -> info option
   val info_of_case : theory -> string -> info option
   val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
   val make_case :  Proof.context -> Datatype_Case.config -> string list -> term ->
     (term * term) list -> term
   val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option

   (case get_info thy name of
     SOME info => info
   | NONE => error ("Unknown datatype " ^ quote name));
 
 fun info_of_constr thy (c, T) =
+  let
+    val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
+  in
+    case body_type T of
+      Type (tyco, _) => AList.lookup (op =) tab tyco
+    | _ => NONE
+  end;
+
+fun info_of_constr_permissive thy (c, T) =
   let
     val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
     val hint = case body_type T of Type (tyco, _) => SOME tyco | _ => NONE;
     val default =
       if null tab then NONE

 
 
 (* translation rules for case *)
 
 fun make_case ctxt = Datatype_Case.make_case
-  (info_of_constr (Proof_Context.theory_of ctxt)) ctxt;
+  (info_of_constr_permissive (Proof_Context.theory_of ctxt)) ctxt;
 
 fun strip_case ctxt = Datatype_Case.strip_case
   (info_of_case (Proof_Context.theory_of ctxt));
 
 fun add_case_tr' case_names thy =

       in (case_name', Datatype_Case.case_tr' info_of_case case_name')
       end) case_names, []) thy;
 
 val trfun_setup =
   Sign.add_advanced_trfuns ([],
-    [(@{syntax_const "_case_syntax"}, Datatype_Case.case_tr true info_of_constr)],
+    [(@{syntax_const "_case_syntax"}, Datatype_Case.case_tr true info_of_constr_permissive)],
     [], []);
 
 
 
 (** document antiquotation **)