src/HOL/Tools/Predicate_Compile/core_data.ML

 
         val pos = Position.thread_data ()
         fun is_intro_of intro =
           let
             val (const, _) = strip_comb (HOLogic.dest_Trueprop (Thm.concl_of intro))
-          in (fst (dest_Const const) = name) end;
+          in dest_Const_name const = name end;
         val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result))
         val index = find_index (fn s => s = name) (#names (fst info))
         val pre_elim = nth (#elims result) index
         val pred = nth (#preds result) index
         val elim_t = mk_casesrule ctxt pred intros

         (is_inductive_predicate ctxt c orelse is_registered ctxt c))
   end;
 
 fun add_intro (opt_case_name, thm) thy =
   let
-    val (name, _) = dest_Const (fst (strip_intro_concl thm))
+    val name = dest_Const_name (fst (strip_intro_concl thm))
     fun cons_intro gr =
       (case try (Graph.get_node gr) name of
         SOME _ =>
           Graph.map_node name (map_pred_data
             (apsnd (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)])))))) gr

                 (((([(opt_case_name, thm)], NONE), false), no_compilation)))) gr)
   in PredData.map cons_intro thy end
 
 fun set_elim thm =
   let
-    val (name, _) =
-      dest_Const (fst (strip_comb (HOLogic.dest_Trueprop (hd (Thm.prems_of thm)))))
+    val name = dest_Const_name (fst (strip_comb (HOLogic.dest_Trueprop (hd (Thm.prems_of thm)))))
   in
     PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (apfst (apsnd (K (SOME thm))))))))
   end
 
 fun register_predicate (constname, intros, elim) thy =

   end
 
 fun register_intros (constname, pre_intros) thy =
   let
     val T = Sign.the_const_type thy constname
-    fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl intr)))
+    fun constname_of_intro intr = dest_Const_name (fst (strip_intro_concl intr))
     val _ = if not (forall (fn intr => constname_of_intro intr = constname) pre_intros) then
       error ("register_intros: Introduction rules of different constants are used\n" ^
         "expected rules for " ^ constname ^ ", but received rules for " ^
           commas (map constname_of_intro pre_intros))
       else ()