# HG changeset patch
# User wenzelm
# Date 1575057424 -3600
# Node ID 592e2afdd50c37e387c28458c9b51b6d29da9dde
# Parent  c7d4f2ab40b9adfb05eb7c029c0372dab0a4fb75
more informative spec rules: optional name;
clarified signature;
more thorough treatment of Thm.trim_context vs. Thm.transfer;

diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Library/old_recdef.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -2842,7 +2842,7 @@
       |> Global_Theory.add_thmss
         (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
       ||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])]
-      ||> Spec_Rules.add_global Spec_Rules.equational_recdef ([lhs], flat rules)
+      ||> Spec_Rules.add_global name Spec_Rules.equational_recdef [lhs] (flat rules)
       ||> null tcs ? Code.declare_default_eqns_global (map (rpair true) (flat rules));
     val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
     val thy3 =
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -1414,10 +1414,10 @@
           |> massage_simple_notes fp_b_name;
 
         val (noted, lthy') = lthy
-          |> Spec_Rules.add Spec_Rules.equational (`(single o lhs_head_of o hd) map_thms)
-          |> fp = Least_FP
-            ? Spec_Rules.add Spec_Rules.equational (`(single o lhs_head_of o hd) rel_code_thms)
-          |> Spec_Rules.add Spec_Rules.equational (`(single o lhs_head_of o hd) set0_thms)
+          |> uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) map_thms)
+          |> fp = Least_FP ?
+              uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) rel_code_thms)
+          |> uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) set0_thms)
           |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (rel_code_thms @ map_thms @ set_thms))
           |> Local_Theory.notes (anonymous_notes @ notes);
 
@@ -2689,7 +2689,7 @@
           |> massage_multi_notes fp_b_names fpTs;
       in
         lthy
-        |> Spec_Rules.add Spec_Rules.equational (recs, flat rec_thmss)
+        |> Spec_Rules.add "" Spec_Rules.equational recs (flat rec_thmss)
         |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat rec_thmss))
         |> Local_Theory.notes (common_notes @ notes)
         (* for "datatype_realizer.ML": *)
@@ -2869,7 +2869,7 @@
           |> massage_multi_notes fp_b_names fpTs;
       in
         lthy
-        |> fold (curry (Spec_Rules.add Spec_Rules.equational) corecs)
+        |> fold (Spec_Rules.add "" Spec_Rules.equational corecs)
           [flat corec_sel_thmss, flat corec_thmss]
         |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) corec_code_thms)
         |> Local_Theory.notes (common_notes @ notes)
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -2157,7 +2157,7 @@
         |> Spec_Rules.add Spec_Rules.equational ([fun_t0], flat sel_thmss)
         |> Spec_Rules.add Spec_Rules.equational ([fun_t0], flat ctr_thmss)
 *)
-        |> Spec_Rules.add Spec_Rules.equational ([fun_t0], [code_thm])
+        |> Spec_Rules.add "" Spec_Rules.equational [fun_t0] [code_thm]
         |> plugins code_plugin ? Code.declare_default_eqns [(code_thm, true)]
         |> Local_Theory.notes (anonymous_notes @ notes)
         |> snd
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -1533,9 +1533,9 @@
         val fun_ts0 = map fst def_infos;
       in
         lthy
-        |> Spec_Rules.add (Spec_Rules.equational_primcorec primcorec_types) (fun_ts0, flat sel_thmss)
-        |> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat ctr_thmss)
-        |> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat code_thmss)
+        |> Spec_Rules.add "" (Spec_Rules.equational_primcorec primcorec_types) fun_ts0 (flat sel_thmss)
+        |> Spec_Rules.add "" Spec_Rules.equational fun_ts0 (flat ctr_thmss)
+        |> Spec_Rules.add "" Spec_Rules.equational fun_ts0 (flat code_thmss)
         |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat code_thmss))
         |> Local_Theory.notes (anonymous_notes @ common_notes @ notes)
         |> snd
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -637,6 +637,7 @@
     val transfer = exists (can (fn Transfer_Option => ())) opts;
 
     val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
+    val spec_name = Local_Theory.full_name lthy (Binding.conglomerate (map (#1 o #1) fixes));
 
     val mk_notes =
       flat oooo @{map 4} (fn js => fn prefix => fn qualify => fn thms =>
@@ -654,7 +655,7 @@
     lthy
     |> primrec_simple0 int plugins nonexhaustive transfer fixes (map snd specs)
     |-> (fn {prefix = (names, qualifys), types, result = (ts, defs, (jss, simpss))} =>
-      Spec_Rules.add (Spec_Rules.equational_primrec types) (ts, flat simpss)
+      Spec_Rules.add spec_name (Spec_Rules.equational_primrec types) ts (flat simpss)
       #> Local_Theory.notes (mk_notes jss names qualifys simpss)
       #-> (fn notes =>
         plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (maps snd notes))
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -373,8 +373,8 @@
 
       val (noted, lthy3) =
         lthy2
-        |> Spec_Rules.add Spec_Rules.equational (size_consts, size_simps)
-        |> Spec_Rules.add Spec_Rules.equational (overloaded_size_consts, overloaded_size_simps)
+        |> Spec_Rules.add "" Spec_Rules.equational size_consts size_simps
+        |> Spec_Rules.add "" Spec_Rules.equational overloaded_size_consts overloaded_size_simps
         |> Code.declare_default_eqns (map (rpair true) (flat size_thmss))
           (*Ideally, this would be issued only if the "code" plugin is enabled.*)
         |> Local_Theory.notes notes;
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -1111,10 +1111,10 @@
             ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
 
         val (noted, lthy') = lthy
-          |> Spec_Rules.add Spec_Rules.equational ([casex], case_thms)
-          |> fold (Spec_Rules.add Spec_Rules.equational)
+          |> Spec_Rules.add "" Spec_Rules.equational [casex] case_thms
+          |> fold (uncurry (Spec_Rules.add "" Spec_Rules.equational))
             (AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms))
-          |> fold (Spec_Rules.add Spec_Rules.equational)
+          |> fold (uncurry (Spec_Rules.add "" Spec_Rules.equational))
             (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
           |> Local_Theory.declaration {syntax = false, pervasive = true}
             (fn phi => Case_Translation.register
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/Function/function.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -211,7 +211,7 @@
              lthy2
              |> Local_Theory.declaration {syntax = false, pervasive = false}
                (fn phi => add_function_data (transform_function_data phi info'))
-             |> Spec_Rules.add Spec_Rules.equational_recdef (fs, tsimps))
+             |> Spec_Rules.add "" Spec_Rules.equational_recdef fs tsimps)
           end)
       end
   in
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -302,7 +302,7 @@
     val ((_, [rec_rule']), lthy'') = lthy' |> Local_Theory.note (eq_abinding, [rec_rule])
   in
     lthy''
-    |> Spec_Rules.add Spec_Rules.equational_recdef ([f], [rec_rule'])
+    |> Spec_Rules.add "" Spec_Rules.equational_recdef [f] [rec_rule']
     |> note_qualified ("simps", [rec_rule'])
     |> note_qualified ("mono", [mono_thm])
     |> (case raw_induct of NONE => I | SOME thm => note_qualified ("raw_induct", [thm]))
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -1353,8 +1353,8 @@
 
 fun all_nondefs_of ctxt subst =
   ctxt |> Spec_Rules.get
-       |> filter (Spec_Rules.is_unknown o fst)
-       |> maps (snd o snd)
+       |> filter (Spec_Rules.is_unknown o #rough_classification)
+       |> maps #rules
        |> filter_out (is_built_in_theory o Thm.theory_id)
        |> map (subst_atomic subst o Thm.prop_of)
 
@@ -1945,10 +1945,9 @@
 fun inductive_intro_table ctxt subst def_tables =
   let val thy = Proof_Context.theory_of ctxt in
     def_table_for
-        (maps (map (unfold_mutually_inductive_preds thy def_tables o Thm.prop_of)
-               o snd o snd)
-         (filter ((Spec_Rules.is_inductive orf Spec_Rules.is_co_inductive) o #1)
-           (Spec_Rules.get ctxt))) subst
+      (maps (map (unfold_mutually_inductive_preds thy def_tables o Thm.prop_of) o #rules)
+        (filter (Spec_Rules.is_relational o #rough_classification)
+         (Spec_Rules.get ctxt))) subst
   end
 
 fun ground_theorem_table thy =
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/Nunchaku/nunchaku_collect.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -479,7 +479,7 @@
       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
@@ -496,18 +496,21 @@
 
     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 ();
@@ -537,10 +540,9 @@
 
 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;
 
@@ -961,7 +963,7 @@
                                     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 ()
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/Old_Datatype/old_primrec.ML
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -278,6 +278,7 @@
 fun gen_primrec prep_spec int raw_fixes raw_spec lthy =
   let
     val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
+    val spec_name = Local_Theory.full_name lthy (Binding.conglomerate (map (#1 o #1) fixes));
     fun attr_bindings prefix = map (fn ((b, attrs), _) =>
       (Binding.qualify false prefix b, attrs)) spec;
     fun simp_attr_binding prefix =
@@ -286,7 +287,7 @@
     lthy
     |> primrec_simple int fixes (map snd spec)
     |-> (fn {prefix, types, result = (ts, simps)} =>
-      Spec_Rules.add (Spec_Rules.equational_primrec types) (ts, simps)
+      Spec_Rules.add spec_name (Spec_Rules.equational_primrec types) ts simps
       #> fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps)
       #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')
         #-> (fn (_, simps'') => 
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -212,7 +212,7 @@
         [] =>
           (case Spec_Rules.retrieve ctxt t of
             [] => error ("No specification for " ^ Syntax.string_of_term_global thy t)
-          | ((_, (_, ths)) :: _) => filter_defs ths)
+          | ({rules = ths, ...} :: _) => filter_defs ths)
       | ths => ths)
     val _ =
       if show_intermediate_results options then
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -317,12 +317,12 @@
 *)
         val specs = Spec_Rules.get ctxt
         val (rec_defs, nonrec_defs) = specs
-          |> filter (Spec_Rules.is_equational o fst)
-          |> maps (snd o snd)
+          |> filter (Spec_Rules.is_equational o #rough_classification)
+          |> maps #rules
           |> List.partition (is_rec_def o Thm.prop_of)
         val spec_intros = specs
-          |> filter ((Spec_Rules.is_inductive orf Spec_Rules.is_co_inductive) o fst)
-          |> maps (snd o snd)
+          |> filter (Spec_Rules.is_relational o #rough_classification)
+          |> maps #rules
       in
         Termtab.empty
         |> fold (add Simp o snd) simps
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/inductive.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -71,7 +71,7 @@
     term list -> (Attrib.binding * term) list -> thm list ->
     term list -> (binding * mixfix) list ->
     local_theory -> result * local_theory
-  val declare_rules: binding -> bool -> bool -> string list -> term list ->
+  val declare_rules: binding -> bool -> bool -> string -> string list -> term list ->
     thm list -> binding list -> Token.src list list -> (thm * string list * int) list ->
     thm list -> thm -> local_theory -> thm list * thm list * thm list * thm * thm list * local_theory
   val add_ind_def: add_ind_def
@@ -1017,7 +1017,7 @@
       list_comb (rec_const, params), preds, argTs, bs, xs)
   end;
 
-fun declare_rules rec_binding coind no_ind cnames
+fun declare_rules rec_binding coind no_ind spec_name cnames
     preds intrs intr_bindings intr_atts elims eqs raw_induct lthy =
   let
     val rec_name = Binding.name_of rec_binding;
@@ -1041,8 +1041,8 @@
 
     val (intrs', lthy1) =
       lthy |>
-      Spec_Rules.add
-        (if coind then Spec_Rules.Co_Inductive else Spec_Rules.Inductive) (preds, intrs) |>
+      Spec_Rules.add spec_name
+        (if coind then Spec_Rules.Co_Inductive else Spec_Rules.Inductive) preds intrs |>
       Local_Theory.notes
         (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
           map (fn th => [([th], @{attributes [Pure.intro?]})]) intrs) |>>
@@ -1099,6 +1099,7 @@
     val _ = message (quiet_mode andalso not verbose)
       ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
 
+    val spec_name = Local_Theory.full_name lthy (Binding.conglomerate (map #1 cnames_syn));
     val cnames = map (Local_Theory.full_name lthy o #1) cnames_syn;  (* FIXME *)
     val ((intr_names, intr_atts), intr_ts) =
       apfst split_list (split_list (map (check_rule lthy cs params) intros));
@@ -1131,7 +1132,7 @@
 
     val (intrs'', elims'', eqs', induct, inducts, lthy3) =
       declare_rules rec_binding coind no_ind
-        cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1;
+        spec_name cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1;
 
     val result =
       {preds = preds,
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -503,10 +503,11 @@
     val rec_name =
       if Binding.is_empty alt_name then Binding.conglomerate (map #1 cnames_syn) else alt_name;
     val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
+    val spec_name = Local_Theory.full_name lthy3 (Binding.conglomerate (map #1 cnames_syn));
     val (intr_names, intr_atts) = split_list (map fst intros);
     val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
     val (intrs', elims', eqs', induct, inducts, lthy4) =
-      Inductive.declare_rules rec_name coind no_ind cnames (map fst defs)
+      Inductive.declare_rules rec_name coind no_ind spec_name cnames (map fst defs)
         (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
         (map (fn th => (to_set [] (Context.Proof lthy3) th,
            map (fst o fst) (fst (Rule_Cases.get th)),
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/HOL/Tools/record.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -1813,9 +1813,8 @@
   | lhs_of_equation (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _)) = t;
 
 fun add_spec_rule rule =
-  let val head = head_of (lhs_of_equation (Thm.prop_of rule)) in
-    Spec_Rules.add_global Spec_Rules.equational ([head], [rule])
-  end;
+  let val head = head_of (lhs_of_equation (Thm.prop_of rule))
+  in Spec_Rules.add_global "" Spec_Rules.equational [head] [rule] end;
 
 (* definition *)
 
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/Pure/Isar/spec_rules.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -21,14 +21,16 @@
   val is_equational: rough_classification -> bool
   val is_inductive: rough_classification -> bool
   val is_co_inductive: rough_classification -> bool
+  val is_relational: rough_classification -> bool
   val is_unknown: rough_classification -> bool
-  type spec = rough_classification * (term list * thm list)
+  type spec =
+    {name: string, rough_classification: rough_classification, terms: term list, rules: thm list}
   val get: Proof.context -> spec list
   val get_global: theory -> spec list
   val retrieve: Proof.context -> term -> spec list
   val retrieve_global: theory -> term -> spec list
-  val add: rough_classification -> term list * thm list -> local_theory -> local_theory
-  val add_global: rough_classification -> term list * thm list -> theory -> theory
+  val add: string -> rough_classification -> term list -> thm list -> local_theory -> local_theory
+  val add_global: string -> rough_classification -> term list -> thm list -> theory -> theory
 end;
 
 structure Spec_Rules: SPEC_RULES =
@@ -64,23 +66,28 @@
 val is_equational = fn Equational _ => true | _ => false;
 val is_inductive = fn Inductive => true | _ => false;
 val is_co_inductive = fn Co_Inductive => true | _ => false;
+val is_relational = is_inductive orf is_co_inductive;
 val is_unknown = fn Unknown => true | _ => false;
 
 
 (* rules *)
 
-type spec = rough_classification * (term list * thm list);
+type spec =
+  {name: string, rough_classification: rough_classification, terms: term list, rules: thm list};
+
+fun eq_spec (specs: spec * spec) =
+  (op =) (apply2 #name specs) andalso
+  is_equal (rough_classification_ord (apply2 #rough_classification specs)) andalso
+  eq_list (op aconv) (apply2 #terms specs) andalso
+  eq_list Thm.eq_thm_prop (apply2 #rules specs);
+
+fun map_spec_rules f ({name, rough_classification, terms, rules}: spec) : spec =
+  {name = name, rough_classification = rough_classification, terms = terms, rules = map f rules};
 
 structure Rules = Generic_Data
 (
   type T = spec Item_Net.T;
-  val empty : T =
-    Item_Net.init
-      (fn ((c1, (ts1, ths1)), (c2, (ts2, ths2))) =>
-        is_equal (rough_classification_ord (c1, c2)) andalso
-        eq_list (op aconv) (ts1, ts2) andalso
-        eq_list Thm.eq_thm_prop (ths1, ths2))
-      (#1 o #2);
+  val empty : T = Item_Net.init eq_spec #terms;
   val extend = I;
   val merge = Item_Net.merge;
 );
@@ -92,7 +99,10 @@
   let
     val thy = Context.theory_of context;
     val transfer = Global_Theory.transfer_theories thy;
-  in Item_Net.content (Rules.get context) |> (map o apsnd o apsnd o map) transfer end;
+  in
+    Item_Net.content (Rules.get context)
+    |> (map o map_spec_rules) transfer
+  end;
 
 val get = get_generic o Context.Proof;
 val get_global = get_generic o Context.Theory;
@@ -102,7 +112,7 @@
 
 fun retrieve_generic context =
   Item_Net.retrieve (Rules.get context)
-  #> (map o apsnd o apsnd o map) (Thm.transfer'' context);
+  #> (map o map_spec_rules) (Thm.transfer'' context);
 
 val retrieve = retrieve_generic o Context.Proof;
 val retrieve_global = retrieve_generic o Context.Theory;
@@ -110,22 +120,27 @@
 
 (* add *)
 
-fun add class (ts, ths) lthy =
-  let
-    val cts = map (Thm.cterm_of lthy) ts;
-  in
+fun add name rough_classification terms rules lthy =
+  let val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules) in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
-      (fn phi =>
+      (fn phi => fn context =>
         let
-          val (ts', ths') =
-            Morphism.fact phi (map Drule.mk_term cts @ ths)
-            |> chop (length cts)
+          val (terms', rules') =
+            map (Thm.transfer (Context.theory_of context)) thms0
+            |> Morphism.fact phi
+            |> chop (length terms)
             |>> map (Thm.term_of o Drule.dest_term)
             ||> map Thm.trim_context;
-        in Rules.map (Item_Net.update (class, (ts', ths'))) end)
+        in
+          context |> (Rules.map o Item_Net.update)
+            {name = name, rough_classification = rough_classification,
+              terms = terms', rules = rules'}
+        end)
   end;
 
-fun add_global class spec =
-  Context.theory_map (Rules.map (Item_Net.update (class, (apsnd o map) Thm.trim_context spec)));
+fun add_global name rough_classification terms rules =
+  (Context.theory_map o Rules.map o Item_Net.update)
+    {name = name, rough_classification = rough_classification,
+      terms = terms, rules = map Thm.trim_context rules};
 
 end;
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/Pure/Isar/specification.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -229,7 +229,7 @@
     (*facts*)
     val (facts, facts_lthy) = axioms_thy
       |> Named_Target.theory_init
-      |> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms)
+      |> Spec_Rules.add "" Spec_Rules.Unknown consts (maps (maps #1 o #2) axioms)
       |> Local_Theory.notes axioms;
 
   in ((consts, map (the_single o #2) facts), Local_Theory.exit_global facts_lthy) end;
@@ -258,12 +258,14 @@
           else
             error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
               Position.here (Binding.pos_of b)));
+    val const_name = Local_Theory.full_name lthy b;
+
     val name = Thm.def_binding_optional b a;
     val ((lhs, (_, raw_th)), lthy2) = lthy
       |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
 
     val th = prove lthy2 raw_th;
-    val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.equational ([lhs], [th]);
+    val lthy3 = lthy2 |> Spec_Rules.add const_name Spec_Rules.equational [lhs] [th];
 
     val ([(def_name, [th'])], lthy4) = lthy3
       |> Local_Theory.notes [((name, atts), [([th], [])])];
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/Pure/Proof/extraction.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -815,14 +815,16 @@
         val ft = Type.legacy_freeze t;
         val fu = Type.legacy_freeze u;
         val head = head_of (strip_abs_body fu);
+        val b = Binding.qualified_name (extr_name s vs);
+        val const_name = Sign.full_name thy b;
       in
         thy
-        |> Sign.add_consts [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
+        |> Sign.add_consts [(b, fastype_of ft, NoSyn)]
         |> Global_Theory.add_defs false
            [((Binding.qualified_name (Thm.def_name (extr_name s vs)),
              Logic.mk_equals (head, ft)), [])]
         |-> (fn [def_thm] =>
-           Spec_Rules.add_global Spec_Rules.equational ([head], [def_thm])
+           Spec_Rules.add_global const_name Spec_Rules.equational [head] [def_thm]
            #> Code.declare_default_eqns_global [(def_thm, true)])
       end;
 
diff -r c7d4f2ab40b9 -r 592e2afdd50c src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Fri Nov 29 20:52:28 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Fri Nov 29 20:57:04 2019 +0100
@@ -60,9 +60,10 @@
 fun primrec_types ctxt const =
   Spec_Rules.retrieve ctxt (Const const)
   |> get_first
-    (fn (Spec_Rules.Equational (Spec_Rules.Primrec types), _) => SOME (types, false)
-      | (Spec_Rules.Equational (Spec_Rules.Primcorec types), _) => SOME (types, true)
-      | _ => NONE)
+    (#rough_classification #>
+      (fn Spec_Rules.Equational (Spec_Rules.Primrec types) => SOME (types, false)
+        | Spec_Rules.Equational (Spec_Rules.Primcorec types) => SOME (types, true)
+        | _ => NONE))
   |> the_default ([], false);