# HG changeset patch
# User blanchet
# Date 1418624449 -3600
# Node ID 15c342a9a8e08aa68fb055578be8a332f5979f51
# Parent  705f8aea8d608ec252e73d68ca8b0c50254f5532
correctly apply type substitution before checking for function types

diff -r 705f8aea8d60 -r 15c342a9a8e0 src/HOL/Tools/SMT/smt_datatypes.ML
--- a/src/HOL/Tools/SMT/smt_datatypes.ML	Mon Dec 15 07:20:48 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Mon Dec 15 07:20:49 2014 +0100
@@ -27,23 +27,21 @@
 
 fun get_ctr_sugar_decl ({ctrs = ctrs0, selss = selss0, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
   let
-    fun mk_constr ctr0 sels0 =
-      let
-        val sels = map (Ctr_Sugar.mk_disc_or_sel Ts) sels0
-        val ctr = Ctr_Sugar.mk_ctr Ts ctr0
-        val binder_Ts = binder_types (fastype_of ctr)
-      in
-        mk_selectors T binder_Ts sels #>> pair ctr
-      end
+    val selss = map (map (Ctr_Sugar.mk_disc_or_sel Ts)) selss0
+    val ctrs = map (Ctr_Sugar.mk_ctr Ts) ctrs0
+
+    fun mk_constr ctr sels =
+      mk_selectors T (binder_types (fastype_of ctr)) sels #>> pair ctr
 
-    val selss =
-      if has_duplicates (op aconv) (flat selss0) orelse
-         exists (exists (can (dest_funT o range_type o fastype_of))) selss0 then
-        []
-      else
-        selss0
+    val selss' =
+      (if has_duplicates (op aconv) (flat selss) orelse
+          exists (exists (can (dest_funT o range_type o fastype_of))) selss then
+         []
+       else
+         selss)
+      |> Ctr_Sugar_Util.pad_list [] (length ctrs)
   in
-    @{fold_map 2} mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt
+    @{fold_map 2} mk_constr ctrs selss' ctxt
     |>> (pair T #> single)
   end