clarified: constructors in the sense of the code generator are not invertible;
correct treatment of constructors with same name but different type;
moved doubtful comment to corresponding function call

--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Thu Mar 10 12:33:01 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Thu Mar 10 12:33:04 2016 +0100
@@ -167,7 +167,8 @@
     fold find' xs NONE
   end
   
-fun is_invertible_function ctxt (Const (f, _)) = is_constr ctxt f
+fun is_invertible_function ctxt (Const cT) =
+      is_some (lookup_constr ctxt cT)
   | is_invertible_function ctxt _ = false
 
 fun non_invertible_subterms ctxt (Free _) = []

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Mar 10 12:33:01 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Mar 10 12:33:04 2016 +0100
@@ -43,9 +43,8 @@
   val is_pred_equation : thm -> bool
   val is_intro : string -> thm -> bool
   val is_predT : typ -> bool
-  val get_constrs : theory -> (string * (int * string)) list
-  val is_constrt : theory -> term -> bool
-  val is_constr : Proof.context -> string -> bool
+  val lookup_constr : Proof.context -> (string * typ) -> int option
+  val is_constrt : Proof.context -> term -> bool
   val strip_ex : term -> (string * typ) list * term
   val focus_ex : term -> Name.context -> ((string * typ) list * term) * Name.context
   val strip_all : term -> (string * typ) list * term
@@ -166,8 +165,6 @@
 structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX =
 struct
 
-val no_constr = [@{const_name STR}];
-
 (* general functions *)
 
 fun comb_option f (SOME x1, SOME x2) = SOME (f (x1, x2))
@@ -478,37 +475,32 @@
 fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool})
   | is_predT _ = false
 
-fun get_constrs thy =
+fun lookup_constr ctxt =
   let
-    val ctxt = Proof_Context.init_global thy
-  in
-    Ctr_Sugar.ctr_sugars_of ctxt
-    |> maps (map_filter (try dest_Const) o #ctrs)
-    |> map (apsnd (fn T => (BNF_Util.num_binder_types T, fst (dest_Type (body_type T)))))
-  end
+    val tab = Ctr_Sugar.ctr_sugars_of ctxt
+      |> maps (map_filter (try dest_Const) o #ctrs)
+      |> map (fn (c, T) => ((c, (fst o dest_Type o body_type) T), BNF_Util.num_binder_types T))
+  in fn (c, T) =>
+    case body_type T of
+      Type (Tname, _) => AList.lookup (op =) tab (c, Tname)
+    | _ => NONE
+  end;
 
-(*** check if a term contains only constructor functions ***)
-(* TODO: another copy in the core! *)
-(* FIXME: constructor terms are supposed to be seen in the way the code generator
-  sees constructors.*)
-fun is_constrt thy =
+fun is_constrt ctxt =
   let
-    val cnstrs = get_constrs thy
+    val lookup_constr = lookup_constr ctxt
     fun check t =
       (case strip_comb t of
         (Var _, []) => true
       | (Free _, []) => true
-      | (Const (s, T), ts) =>
-          (case (AList.lookup (op =) cnstrs s, body_type T) of
-            (SOME (i, Tname), Type (Tname', _)) =>
-              length ts = i andalso Tname = Tname' andalso forall check ts
+      | (Const cT, ts) =>
+          (case lookup_constr cT of
+            SOME i =>
+              length ts = i andalso forall check ts
           | _ => false)
       | _ => false)
   in check end
 
-fun is_constr ctxt c =
-  not (member (op =) no_constr c) andalso Code.is_constr (Proof_Context.theory_of ctxt) c;
-
 fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
 
 fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Mar 10 12:33:01 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Mar 10 12:33:04 2016 +0100
@@ -94,6 +94,7 @@
 
 fun flatten thy lookup_pred t (names, prems) =
   let
+    val ctxt = Proof_Context.init_global thy;
     fun lift t (names, prems) =
       (case lookup_pred (Envir.eta_contract t) of
         SOME pred => [(pred, (names, prems))]
@@ -139,7 +140,9 @@
       | flatten' (t as Free _) (names, prems) = [(t, (names, prems))]
       | flatten' (t as Abs _) (names, prems) = [(t, (names, prems))]
       | flatten' (t as _ $ _) (names, prems) =
-      if Predicate_Compile_Aux.is_constrt thy t orelse keep_functions thy t then
+      if is_constrt ctxt t orelse keep_functions thy t then
+       (* FIXME: constructor terms are supposed to be seen in the way the code generator
+          sees constructors?*)
         [(t, (names, prems))]
       else
         case (fst (strip_comb t)) of

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Thu Mar 10 12:33:01 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Thu Mar 10 12:33:04 2016 +0100
@@ -41,19 +41,19 @@
   end
 
 (* patterns only constructed of variables and pairs/tuples are trivial constructor terms*)
-fun is_nontrivial_constrt thy t =
+fun is_nontrivial_constrt ctxt t =
   let
-    val cnstrs = get_constrs thy
+    val lookup_constr = lookup_constr ctxt
     fun check t =
       (case strip_comb t of
         (Var _, []) => (true, true)
       | (Free _, []) => (true, true)
       | (Const (@{const_name Pair}, _), ts) =>
         apply2 (forall I) (split_list (map check ts))
-      | (Const (s, T), ts) =>
-          (case (AList.lookup (op =) cnstrs s, body_type T) of
-            (SOME (i, Tname), Type (Tname', _)) => (false,
-              length ts = i andalso Tname = Tname' andalso forall (snd o check) ts)
+      | (Const cT, ts) =>
+          (case lookup_constr cT of
+            SOME i => (false,
+              length ts = i andalso forall (snd o check) ts)
           | _ => (false, false))
       | _ => (false, false))
   in check t = (false, true) end
@@ -167,7 +167,7 @@
             val Ts = binder_types (Sign.the_const_type thy pred_name)
             val pats = restrict_pattern thy Ts args
           in
-            if (exists (is_nontrivial_constrt thy) pats)
+            if (exists (is_nontrivial_constrt ctxt) pats)
               orelse (has_duplicates (op =) (fold add_vars pats [])) then
               let
                 val thy' =