src/HOL/Tools/Nunchaku/nunchaku_collect.ML

 
     fun subst_of t0 =
       try (Sign.typ_match thy (fastype_of t0, T)) Vartab.empty;
 
     fun process_spec _ (res as SOME _) = res
-      | process_spec (classif, (ts0, ths as _ :: _)) NONE =
+      | process_spec {rough_classification = classif, terms = ts0, rules = ths as _ :: _, ...} NONE =
         (case get_first subst_of ts0 of
           SOME subst =>
           (let
              val ts = map (Envir.subst_term_types subst) ts0;
              val poly_props = map Thm.prop_of ths;

         | NONE => NONE)
       | process_spec _ NONE = NONE;
 
     fun spec_rules () =
       Spec_Rules.retrieve ctxt (Const x)
-      |> sort (Spec_Rules.rough_classification_ord o apply2 fst);
+      |> sort (Spec_Rules.rough_classification_ord o apply2 #rough_classification);
 
     val specs =
       if s = \<^const_name>\<open>The\<close> then
-        [(Spec_Rules.Unknown, ([Logic.varify_global \<^term>\<open>The\<close>], [@{thm theI_unique}]))]
+        [{name = "", rough_classification = Spec_Rules.Unknown,
+          terms = [Logic.varify_global \<^term>\<open>The\<close>],
+          rules = [@{thm theI_unique}]}]
       else if s = \<^const_name>\<open>finite\<close> then
         let val card = card_of_type ctxt T in
           if card = Inf orelse card = Fin_or_Inf then
             spec_rules ()
           else
-            [(Spec_Rules.equational, ([Logic.varify_global \<^term>\<open>finite\<close>],
-               [Skip_Proof.make_thm thy (Logic.varify_global \<^prop>\<open>finite A = True\<close>)]))]
+            [{name = "", rough_classification = Spec_Rules.equational,
+              terms = [Logic.varify_global \<^term>\<open>finite\<close>],
+              rules = [Skip_Proof.make_thm thy (Logic.varify_global \<^prop>\<open>finite A = True\<close>)]}]
         end
       else
         spec_rules ();
   in
     fold process_spec specs NONE

 fun is_builtin_theory thy_id =
   Context.subthy_id (thy_id, Context.theory_id \<^theory>\<open>Hilbert_Choice\<close>);
 
 val orphan_axioms_of =
   Spec_Rules.get
-  #> filter (Spec_Rules.is_unknown o fst)
-  #> map snd
-  #> filter (null o fst)
-  #> maps snd
+  #> filter (Spec_Rules.is_unknown o #rough_classification)
+  #> filter (null o #terms)
+  #> maps #rules
   #> filter_out (is_builtin_theory o Thm.theory_id)
   #> map Thm.prop_of;
 
 fun keys_of _ (ITVal (T, _)) = [key_of_typ T]
   | keys_of _ (ITypedef {abs_typ, ...}) = [key_of_typ abs_typ]

                               [IRec (map2 (fn const => fn props =>
                                    {const = const, props = props,
                                     pat_complete = is_apparently_pat_complete ctxt props})
                                  consts propss)])
                            | NONE => def_or_spec ())
-                         else if (Spec_Rules.is_inductive orf Spec_Rules.is_co_inductive) classif
+                         else if Spec_Rules.is_relational classif
                          then
                            if is_inductive_set_intro (hd props) then
                              def_or_spec ()
                            else
                              (case partition_props consts props of