src/ZF/Tools/inductive_package.ML

   val dummy = rec_hds |> forall (fn t => is_Const t orelse
       error ("Recursive set not previously declared as constant: " ^
                    Syntax.string_of_term ctxt0 t));
 
   (*Now we know they are all Consts, so get their names, type and params*)
-  val rec_names = map (#1 o dest_Const) rec_hds
+  val rec_names = map dest_Const_name rec_hds
   and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
 
   val rec_base_names = map Long_Name.base_name rec_names;
   val dummy = rec_base_names |> forall (fn a => Symbol_Pos.is_identifier a orelse
     error ("Base name of recursive set not an identifier: " ^ a));

        and a conclusion for the simultaneous induction rule.
        NOTE.  This will not work for mutually recursive predicates.  Previously
        a summand 'domt' was also an argument, but this required the domain of
        mutual recursion to invariably be a disjoint sum.*)
      fun mk_predpair rec_tm =
-       let val rec_name = (#1 o dest_Const o head_of) rec_tm
+       let val rec_name = dest_Const_name (head_of rec_tm)
            val pfree = Free(pred_name ^ "_" ^ Long_Name.base_name rec_name,
                             elem_factors ---> \<^Type>\<open>o\<close>)
            val qconcl =
              fold_rev (FOLogic.mk_all o Term.dest_Free) elem_frees
                \<^Const>\<open>imp for \<^Const>\<open>mem for elem_tuple rec_tm\<close> \<open>list_comb (pfree, elem_frees)\<close>\<close>