# HG changeset patch
# User krauss
# Date 1309187044 -7200
# Node ID 023a1d1f97bdd52c9ce32d5103d1260c8df131e1
# Parent  66f8cf4f82d906c38527a3fdf84fdc6483e68903
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
renamed old version to info_of_constr_permissive, reflecting its semantics

diff -r 66f8cf4f82d9 -r 023a1d1f97bd src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Mon Jun 27 14:56:39 2011 +0200
+++ b/src/HOL/Inductive.thy	Mon Jun 27 17:04:04 2011 +0200
@@ -297,7 +297,7 @@
     let
       (* FIXME proper name context!? *)
       val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
-      val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
+      val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr_permissive ctxt [x, cs];
     in lambda x ft end
 in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
 *}
diff -r 66f8cf4f82d9 -r 023a1d1f97bd src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Jun 27 14:56:39 2011 +0200
+++ b/src/HOL/List.thy	Mon Jun 27 17:04:04 2011 +0200
@@ -391,7 +391,7 @@
         Syntax.const @{syntax_const "_case1"} $
           Syntax.const @{const_syntax dummy_pattern} $ NilC;
       val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
-      val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs];
+      val ft = Datatype_Case.case_tr false Datatype.info_of_constr_permissive ctxt [x, cs];
     in lambda x ft end;
 
   fun abs_tr ctxt (p as Free (s, T)) e opti =
diff -r 66f8cf4f82d9 -r 023a1d1f97bd src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon Jun 27 14:56:39 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon Jun 27 17:04:04 2011 +0200
@@ -23,6 +23,7 @@
   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 ->
@@ -70,6 +71,15 @@
 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
@@ -216,7 +226,7 @@
 (* 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));
@@ -230,7 +240,7 @@
 
 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)],
     [], []);