ported predicate compiler to 'ctr_sugar'
authorblanchet
Wed Feb 12 08:35:56 2014 +0100 (2014-02-12)
changeset 553995c8e91f884af
parent 55398 67e9fdd9ae9e
child 55400 1e8dd9cd320b
ported predicate compiler to 'ctr_sugar'
* * *
ported predicate compiler to 'ctr_sugar', part 2
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/mode_inference.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -511,13 +511,6 @@
     1.4  
     1.5  fun mk_lim_relname T = "lim_" ^  mk_relname T
     1.6  
     1.7 -(* This is copied from "pat_completeness.ML" *)
     1.8 -fun inst_constrs_of thy (T as Type (name, _)) =
     1.9 -  map (fn (Cn,CT) =>
    1.10 -    Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
    1.11 -    (the (Datatype.get_constrs thy name))
    1.12 -  | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
    1.13 -
    1.14  fun is_recursive_constr T (Const (constr_name, T')) = member (op =) (binder_types T') T
    1.15    
    1.16  fun mk_ground_impl ctxt limited_types (T as Type (Tcon, Targs)) (seen, constant_table) =
    1.17 @@ -549,7 +542,7 @@
    1.18          in
    1.19            (clause :: flat rec_clauses, (seen', constant_table''))
    1.20          end
    1.21 -      val constrs = inst_constrs_of (Proof_Context.theory_of ctxt) T
    1.22 +      val constrs = Function_Lib.inst_constrs_of (Proof_Context.theory_of ctxt) T
    1.23        val constrs' = (constrs ~~ map (is_recursive_constr T) constrs)
    1.24          |> (fn cs => filter_out snd cs @ filter snd cs)
    1.25        val (clauses, constant_table') =
     2.1 --- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Wed Feb 12 08:35:56 2014 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Wed Feb 12 08:35:56 2014 +0100
     2.3 @@ -183,19 +183,19 @@
     2.4    | collect_non_invertible_subterms ctxt t (names, eqs) =
     2.5      case (strip_comb t) of (f, args) =>
     2.6        if is_invertible_function ctxt f then
     2.7 -          let
     2.8 -            val (args', (names', eqs')) =
     2.9 -              fold_map (collect_non_invertible_subterms ctxt) args (names, eqs)
    2.10 -          in
    2.11 -            (list_comb (f, args'), (names', eqs'))
    2.12 -          end
    2.13 -        else
    2.14 -          let
    2.15 -            val s = singleton (Name.variant_list names) "x"
    2.16 -            val v = Free (s, fastype_of t)
    2.17 -          in
    2.18 -            (v, (s :: names, HOLogic.mk_eq (v, t) :: eqs))
    2.19 -          end
    2.20 +        let
    2.21 +          val (args', (names', eqs')) =
    2.22 +            fold_map (collect_non_invertible_subterms ctxt) args (names, eqs)
    2.23 +        in
    2.24 +          (list_comb (f, args'), (names', eqs'))
    2.25 +        end
    2.26 +      else
    2.27 +        let
    2.28 +          val s = singleton (Name.variant_list names) "x"
    2.29 +          val v = Free (s, fastype_of t)
    2.30 +        in
    2.31 +          (v, (s :: names, HOLogic.mk_eq (v, t) :: eqs))
    2.32 +        end
    2.33  (*
    2.34    if is_constrt thy t then (t, (names, eqs)) else
    2.35      let
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Feb 12 08:35:56 2014 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Feb 12 08:35:56 2014 +0100
     3.3 @@ -47,6 +47,7 @@
     3.4    val is_pred_equation : thm -> bool
     3.5    val is_intro : string -> thm -> bool
     3.6    val is_predT : typ -> bool
     3.7 +  val get_constrs : theory -> (string * (int * string)) list
     3.8    val is_constrt : theory -> term -> bool
     3.9    val is_constr : Proof.context -> string -> bool
    3.10    val strip_ex : term -> (string * typ) list * term
    3.11 @@ -477,15 +478,22 @@
    3.12  fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool})
    3.13    | is_predT _ = false
    3.14  
    3.15 +fun get_constrs thy =
    3.16 +  let
    3.17 +    val ctxt = Proof_Context.init_global thy
    3.18 +  in
    3.19 +    Ctr_Sugar.ctr_sugars_of ctxt
    3.20 +    |> maps (map_filter (try dest_Const) o #ctrs)
    3.21 +    |> map (apsnd (fn T => (BNF_Util.num_binder_types T, fst (dest_Type (body_type T)))))
    3.22 +  end
    3.23 +
    3.24  (*** check if a term contains only constructor functions ***)
    3.25  (* TODO: another copy in the core! *)
    3.26  (* FIXME: constructor terms are supposed to be seen in the way the code generator
    3.27    sees constructors.*)
    3.28  fun is_constrt thy =
    3.29    let
    3.30 -    val cnstrs = flat (maps
    3.31 -      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
    3.32 -      (Symtab.dest (Datatype.get_all thy)));
    3.33 +    val cnstrs = get_constrs thy
    3.34      fun check t = (case strip_comb t of
    3.35          (Var _, []) => true
    3.36        | (Free _, []) => true
    3.37 @@ -495,23 +503,6 @@
    3.38        | _ => false)
    3.39    in check end;
    3.40  
    3.41 -(* returns true if t is an application of an datatype constructor *)
    3.42 -(* which then consequently would be splitted *)
    3.43 -(* else false *)
    3.44 -(*
    3.45 -fun is_constructor thy t =
    3.46 -  if (is_Type (fastype_of t)) then
    3.47 -    (case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of
    3.48 -      NONE => false
    3.49 -    | SOME info => (let
    3.50 -      val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
    3.51 -      val (c, _) = strip_comb t
    3.52 -      in (case c of
    3.53 -        Const (name, _) => name mem_string constr_consts
    3.54 -        | _ => false) end))
    3.55 -  else false
    3.56 -*)
    3.57 -
    3.58  val is_constr = Code.is_constr o Proof_Context.theory_of;
    3.59  
    3.60  fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
    3.61 @@ -601,7 +592,8 @@
    3.62      |> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
    3.63        @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
    3.64  
    3.65 -fun find_split_thm thy (Const (name, _)) = Option.map #split (Datatype.info_of_case thy name)
    3.66 +fun find_split_thm thy (Const (name, _)) =
    3.67 +    Option.map #split (Ctr_Sugar.ctr_sugar_of_case (Proof_Context.init_global thy) name)
    3.68    | find_split_thm thy _ = NONE
    3.69  
    3.70  (* lifting term operations to theorems *)
    3.71 @@ -880,76 +872,72 @@
    3.72  (** making case distributivity rules **)
    3.73  (*** this should be part of the datatype package ***)
    3.74  
    3.75 -fun datatype_names_of_case_name thy case_name =
    3.76 -  map (#1 o #2) (#descr (the (Datatype.info_of_case thy case_name)))
    3.77 +fun datatype_name_of_case_name thy =
    3.78 +  Ctr_Sugar.ctr_sugar_of_case (Proof_Context.init_global thy)
    3.79 +  #> the #> #ctrs #> hd #> fastype_of #> body_type #> dest_Type #> fst
    3.80  
    3.81 -fun make_case_distribs case_names descr thy =
    3.82 +fun make_case_comb thy Tcon =
    3.83    let
    3.84 -    val case_combs = Datatype_Prop.make_case_combs case_names descr thy "f";
    3.85 -    fun make comb =
    3.86 -      let
    3.87 -        val Type ("fun", [T, T']) = fastype_of comb;
    3.88 -        val (Const (case_name, _), fs) = strip_comb comb
    3.89 -        val used = Term.add_tfree_names comb []
    3.90 -        val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
    3.91 -        val x = Free ("x", T)
    3.92 -        val f = Free ("f", T' --> U)
    3.93 -        fun apply_f f' =
    3.94 -          let
    3.95 -            val Ts = binder_types (fastype_of f')
    3.96 -            val bs = map Bound ((length Ts - 1) downto 0)
    3.97 -          in
    3.98 -            fold_rev absdummy Ts (f $ (list_comb (f', bs)))
    3.99 -          end
   3.100 -        val fs' = map apply_f fs
   3.101 -        val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
   3.102 -      in
   3.103 -        HOLogic.mk_eq (f $ (comb $ x), list_comb (case_c', fs') $ x)
   3.104 -      end
   3.105 +    val ctxt = Proof_Context.init_global thy
   3.106 +    val SOME {casex, ...} = Ctr_Sugar.ctr_sugar_of ctxt Tcon
   3.107 +    val casex' = Type.legacy_freeze casex
   3.108 +    val Ts = BNF_Util.binder_fun_types (fastype_of casex')
   3.109    in
   3.110 -    map make case_combs
   3.111 +    list_comb (casex', map_index (fn (j, T) => Free ("f" ^ string_of_int j,  T)) Ts)
   3.112    end
   3.113  
   3.114 -fun case_rewrites thy Tcon =
   3.115 +fun make_case_distrib thy Tcon =
   3.116    let
   3.117 -    val {descr, case_name, ...} = Datatype.the_info thy Tcon
   3.118 +    val comb = make_case_comb thy Tcon;
   3.119 +    val Type ("fun", [T, T']) = fastype_of comb;
   3.120 +    val (Const (case_name, _), fs) = strip_comb comb
   3.121 +    val used = Term.add_tfree_names comb []
   3.122 +    val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
   3.123 +    val x = Free ("x", T)
   3.124 +    val f = Free ("f", T' --> U)
   3.125 +    fun apply_f f' =
   3.126 +      let
   3.127 +        val Ts = binder_types (fastype_of f')
   3.128 +        val bs = map Bound ((length Ts - 1) downto 0)
   3.129 +      in
   3.130 +        fold_rev absdummy Ts (f $ (list_comb (f', bs)))
   3.131 +      end
   3.132 +    val fs' = map apply_f fs
   3.133 +    val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
   3.134    in
   3.135 -    map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
   3.136 -      (make_case_distribs [case_name] [descr] thy)
   3.137 +    HOLogic.mk_eq (f $ (comb $ x), list_comb (case_c', fs') $ x)
   3.138    end
   3.139  
   3.140 -fun instantiated_case_rewrites thy Tcon =
   3.141 +fun case_rewrite thy Tcon =
   3.142 +  (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
   3.143 +    (make_case_distrib thy Tcon)
   3.144 +
   3.145 +fun instantiated_case_rewrite thy Tcon =
   3.146    let
   3.147 -    val rew_ths = case_rewrites thy Tcon
   3.148 +    val th = case_rewrite thy Tcon
   3.149      val ctxt = Proof_Context.init_global thy
   3.150 -    fun instantiate th =
   3.151 -    let
   3.152 -      val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
   3.153 -      val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
   3.154 -      val ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
   3.155 -      val T' = TFree (tname', HOLogic.typeS)
   3.156 -      val U = TFree (uname, HOLogic.typeS)
   3.157 -      val y = Free (yname, U)
   3.158 -      val f' = absdummy (U --> T') (Bound 0 $ y)
   3.159 -      val th' = Thm.certify_instantiate
   3.160 -        ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
   3.161 -         [((fst (dest_Var f), (U --> T') --> T'), f')]) th
   3.162 -      val [th'] = Variable.export ctxt' ctxt [th']
   3.163 -   in
   3.164 -     th'
   3.165 -   end
   3.166 - in
   3.167 -   map instantiate rew_ths
   3.168 - end
   3.169 +    val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
   3.170 +    val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
   3.171 +    val ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
   3.172 +    val T' = TFree (tname', HOLogic.typeS)
   3.173 +    val U = TFree (uname, HOLogic.typeS)
   3.174 +    val y = Free (yname, U)
   3.175 +    val f' = absdummy (U --> T') (Bound 0 $ y)
   3.176 +    val th' = Thm.certify_instantiate
   3.177 +      ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
   3.178 +       [((fst (dest_Var f), (U --> T') --> T'), f')]) th
   3.179 +    val [th'] = Variable.export ctxt' ctxt [th']
   3.180 +  in
   3.181 +    th'
   3.182 +  end
   3.183  
   3.184  fun case_betapply thy t =
   3.185    let
   3.186      val case_name = fst (dest_Const (fst (strip_comb t)))
   3.187 -    val Tcons = datatype_names_of_case_name thy case_name
   3.188 -    val ths = maps (instantiated_case_rewrites thy) Tcons
   3.189 +    val Tcon = datatype_name_of_case_name thy case_name
   3.190 +    val th = instantiated_case_rewrite thy Tcon
   3.191    in
   3.192 -    Raw_Simplifier.rewrite_term thy
   3.193 -      (map (fn th => th RS @{thm eq_reflection}) ths) [] t
   3.194 +    Raw_Simplifier.rewrite_term thy [th RS @{thm eq_reflection}] [] t
   3.195    end
   3.196  
   3.197  (*** conversions ***)
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 12 08:35:56 2014 +0100
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 12 08:35:56 2014 +0100
     4.3 @@ -814,13 +814,14 @@
     4.4      case T of
     4.5        TFree _ => NONE
     4.6      | Type (Tcon, _) =>
     4.7 -      (case Datatype.get_constrs (Proof_Context.theory_of ctxt) Tcon of
     4.8 +      (case Ctr_Sugar.ctr_sugar_of ctxt Tcon of
     4.9          NONE => NONE
    4.10 -      | SOME cs =>
    4.11 +      | SOME {ctrs, ...} =>
    4.12          (case strip_comb t of
    4.13            (Var _, []) => NONE
    4.14          | (Free _, []) => NONE
    4.15 -        | (Const (c, T), _) => if AList.defined (op =) cs c then SOME (c, T) else NONE))
    4.16 +        | (Const (c, T), _) =>
    4.17 +          if AList.defined (op =) (map_filter (try dest_Const) ctrs) c then SOME (c, T) else NONE))
    4.18    end
    4.19  
    4.20  fun partition_clause ctxt pos moded_clauses =
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Feb 12 08:35:56 2014 +0100
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Feb 12 08:35:56 2014 +0100
     5.3 @@ -260,8 +260,11 @@
     5.4      val ctxt = Proof_Context.init_global thy
     5.5      fun is_nondefining_const (c, _) = member (op =) logic_operator_names c
     5.6      fun has_code_pred_intros (c, _) = can (Core_Data.intros_of ctxt) c
     5.7 -    fun case_consts (c, _) = is_some (Datatype.info_of_case thy c)
     5.8 -    fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T))
     5.9 +    fun case_consts (c, _) = is_some (Ctr_Sugar.ctr_sugar_of_case ctxt c)
    5.10 +    fun is_datatype_constructor (x as (_, T)) =
    5.11 +      (case body_type T of
    5.12 +        Type (Tcon, _) => can (Ctr_Sugar.dest_ctr ctxt Tcon) (Const x)
    5.13 +      | _ => false)
    5.14      fun defiants_of specs =
    5.15        fold (Term.add_consts o prop_of) specs []
    5.16        |> filter_out is_datatype_constructor
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Feb 12 08:35:56 2014 +0100
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Feb 12 08:35:56 2014 +0100
     6.3 @@ -46,30 +46,19 @@
     6.4  
     6.5  (* auxillary functions *)
     6.6  
     6.7 -fun is_Type (Type _) = true
     6.8 -  | is_Type _ = false
     6.9 -
    6.10 -(* returns true if t is an application of an datatype constructor *)
    6.11 +(* returns true if t is an application of a datatype constructor *)
    6.12  (* which then consequently would be splitted *)
    6.13 -(* else false *)
    6.14 -fun is_constructor thy t =
    6.15 -  if (is_Type (fastype_of t)) then
    6.16 -    (case Datatype.get_info thy ((fst o dest_Type o fastype_of) t) of
    6.17 -      NONE => false
    6.18 -    | SOME info => (let
    6.19 -      val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
    6.20 -      val (c, _) = strip_comb t
    6.21 -      in (case c of
    6.22 -        Const (name, _) => member (op =) constr_consts name
    6.23 -        | _ => false) end))
    6.24 -  else false
    6.25 +fun is_constructor ctxt t =
    6.26 +  (case fastype_of t of
    6.27 +    Type (s, _) => s <> @{type_name fun} andalso can (Ctr_Sugar.dest_ctr ctxt s) t
    6.28 +  | _ => false);
    6.29  
    6.30  (* MAJOR FIXME:  prove_params should be simple
    6.31   - different form of introrule for parameters ? *)
    6.32  
    6.33  fun prove_param options ctxt nargs t deriv =
    6.34    let
    6.35 -    val  (f, args) = strip_comb (Envir.eta_contract t)
    6.36 +    val (f, args) = strip_comb (Envir.eta_contract t)
    6.37      val mode = head_mode_of deriv
    6.38      val param_derivations = param_derivations_of deriv
    6.39      val ho_args = ho_args_of mode args
    6.40 @@ -139,15 +128,14 @@
    6.41  
    6.42  fun prove_match options ctxt nargs out_ts =
    6.43    let
    6.44 -    val thy = Proof_Context.theory_of ctxt
    6.45      val eval_if_P =
    6.46        @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp} 
    6.47      fun get_case_rewrite t =
    6.48 -      if (is_constructor thy t) then
    6.49 +      if is_constructor ctxt t then
    6.50          let
    6.51 -          val {case_rewrites, ...} = Datatype.the_info thy (fst (dest_Type (fastype_of t)))
    6.52 +          val SOME {case_thms, ...} = Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type (fastype_of t)))
    6.53          in
    6.54 -          fold (union Thm.eq_thm) (case_rewrites :: map get_case_rewrite (snd (strip_comb t))) []
    6.55 +          fold (union Thm.eq_thm) (case_thms :: map get_case_rewrite (snd (strip_comb t))) []
    6.56          end
    6.57        else []
    6.58      val simprules = insert Thm.eq_thm @{thm "unit.cases"} (insert Thm.eq_thm @{thm "prod.cases"}
    6.59 @@ -309,14 +297,13 @@
    6.60  
    6.61  fun prove_match2 options ctxt out_ts =
    6.62    let
    6.63 -    val thy = Proof_Context.theory_of ctxt
    6.64      fun split_term_tac (Free _) = all_tac
    6.65        | split_term_tac t =
    6.66 -        if (is_constructor thy t) then
    6.67 +        if is_constructor ctxt t then
    6.68            let
    6.69 -            val {case_rewrites, split_asm, ...} =
    6.70 -              Datatype.the_info thy (fst (dest_Type (fastype_of t)))
    6.71 -            val num_of_constrs = length case_rewrites
    6.72 +            val SOME {case_thms, split_asm, ...} =
    6.73 +              Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type (fastype_of t)))
    6.74 +            val num_of_constrs = length case_thms
    6.75              val (_, ts) = strip_comb t
    6.76            in
    6.77              print_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^ 
     7.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Wed Feb 12 08:35:56 2014 +0100
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Wed Feb 12 08:35:56 2014 +0100
     7.3 @@ -41,9 +41,7 @@
     7.4  (* patterns only constructed of variables and pairs/tuples are trivial constructor terms*)
     7.5  fun is_nontrivial_constrt thy t =
     7.6    let
     7.7 -    val cnstrs = flat (maps
     7.8 -      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
     7.9 -      (Symtab.dest (Datatype.get_all thy)));
    7.10 +    val cnstrs = get_constrs thy
    7.11      fun check t = (case strip_comb t of
    7.12          (Var _, []) => (true, true)
    7.13        | (Free _, []) => (true, true)
    7.14 @@ -107,6 +105,7 @@
    7.15  
    7.16  and find_specialisations black_list specs thy =
    7.17    let
    7.18 +    val ctxt = Proof_Context.init_global thy
    7.19      val add_vars = fold_aterms (fn Var v => cons v | _ => I);
    7.20      fun fresh_free T free_names =
    7.21        let
    7.22 @@ -132,10 +131,11 @@
    7.23        | restrict_pattern' thy ((T as TFree _, t) :: Tts) free_names =
    7.24          replace_term_and_restrict thy T t Tts free_names
    7.25        | restrict_pattern' thy ((T as Type (Tcon, _), t) :: Tts) free_names =
    7.26 -        case Datatype.get_constrs thy Tcon of
    7.27 +        case Ctr_Sugar.ctr_sugar_of ctxt Tcon of
    7.28            NONE => replace_term_and_restrict thy T t Tts free_names
    7.29 -        | SOME constrs => (case strip_comb t of
    7.30 -          (Const (s, _), ats) => (case AList.lookup (op =) constrs s of
    7.31 +        | SOME {ctrs, ...} => (case strip_comb t of
    7.32 +          (Const (s, _), ats) =>
    7.33 +          (case AList.lookup (op =) (map_filter (try dest_Const) ctrs) s of
    7.34              SOME constr_T =>
    7.35                let
    7.36                  val (Ts', T') = strip_type constr_T