# HG changeset patch
# User blanchet
# Date 1411566383 -7200
# Node ID cc1bab5558b00497c49db7b54b8653324d1e51b8
# Parent  cac802846ff1bde5ccb50e2e2535b43a115b4ccb
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'

diff -r cac802846ff1 -r cc1bab5558b0 src/HOL/Tools/SMT/smt_datatypes.ML
--- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 24 15:46:11 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 24 15:46:23 2014 +0200
@@ -61,24 +61,29 @@
 
 (* collection of declarations *)
 
-(* Simplification: We assume that every type that is not a codatatype is a datatype (or a
-   record). *)
-fun fp_kind_of ctxt n =
-  (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
-    SOME {fp, ...} => fp
-  | NONE => BNF_Util.Least_FP)
+val extN = "_ext" (* cf. "HOL/Tools/typedef.ML" *)
 
 fun get_decls fp T n Ts ctxt =
   let
-    fun fallback () =
+    fun maybe_typedef () =
       (case Typedef.get_info ctxt n of
         [] => ([], ctxt)
       | info :: _ => (get_typedef_decl info T Ts, ctxt))
   in
-    (case Ctr_Sugar.ctr_sugar_of ctxt n of
-      SOME (ctr_sugar as {T = U as Type (_, Us), ...}) =>
-      if fp_kind_of ctxt n = fp then get_ctr_sugar_decl ctr_sugar T Ts ctxt else fallback ()
-    | NONE => fallback ())
+    (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
+      SOME {fp = fp', ctr_sugar, ...} =>
+      if fp' = fp then get_ctr_sugar_decl ctr_sugar T Ts ctxt else ([], ctxt)
+    | NONE =>
+      if fp = BNF_Util.Least_FP then
+        if String.isSuffix extN n then
+          (* for records (FIXME: hack) *)
+          (case Ctr_Sugar.ctr_sugar_of ctxt n of
+            SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt
+          | NONE => maybe_typedef ())
+        else
+          maybe_typedef ()
+      else
+        ([], ctxt))
   end
 
 fun add_decls fp T (declss, ctxt) =