# HG changeset patch
# User wenzelm
# Date 1575382830 -3600
# Node ID 35e465677a268a24540359968283a828e4209d8c
# Parent  6617fb368a060f479be76a3444130860204a8896# Parent  73b313432d8af791396d5a3e600d3b30b64e30a7
merged

diff -r 6617fb368a06 -r 35e465677a26 src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Library/old_recdef.ML	Tue Dec 03 15:20:30 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 name Spec_Rules.equational_recdef [lhs] (flat rules)
+      ||> Spec_Rules.add_global (Binding.name bname) 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 6617fb368a06 -r 35e465677a26 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Dec 03 15:20:30 2019 +0100
@@ -1414,10 +1414,13 @@
           |> massage_simple_notes fp_b_name;
 
         val (noted, lthy') = lthy
-          |> uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) map_thms)
+          |> uncurry (Spec_Rules.add Binding.empty 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)
+              uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational)
+                (`(single o lhs_head_of o hd) rel_code_thms)
+          |> uncurry (Spec_Rules.add Binding.empty 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 +2692,7 @@
           |> massage_multi_notes fp_b_names fpTs;
       in
         lthy
-        |> Spec_Rules.add "" Spec_Rules.equational recs (flat rec_thmss)
+        |> Spec_Rules.add Binding.empty 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 +2872,7 @@
           |> massage_multi_notes fp_b_names fpTs;
       in
         lthy
-        |> fold (Spec_Rules.add "" Spec_Rules.equational corecs)
+        |> fold (Spec_Rules.add Binding.empty 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 6617fb368a06 -r 35e465677a26 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Dec 03 15:20:30 2019 +0100
@@ -1630,21 +1630,21 @@
 
     val ssig_bnf = #fp_bnf ssig_fp_sugar;
 
-    val (dead_ssig_bnf, lthy) = bnf_kill_all_but 1 ssig_bnf lthy;
+    val (dead_ssig_bnf, lthy') = bnf_kill_all_but 1 ssig_bnf lthy;
 
     val dead_pre_rel = mk_rel preT dead_pre_bnf;
     val dead_k_rel = mk_rel k_T dead_k_bnf;
     val dead_ssig_rel = mk_rel ssig_T dead_ssig_bnf;
 
-    val (((parametric_consts, rho_rhs), rho_data), lthy) =
-      extract_rho_from_equation friend_parse_info fun_b version Y preT ssig_T fun_t parsed_eq lthy;
+    val (((parametric_consts, rho_rhs), rho_data), lthy'') =
+      extract_rho_from_equation friend_parse_info fun_b version Y preT ssig_T fun_t parsed_eq lthy';
 
-    val const_transfer_goals = map (mk_const_transfer_goal lthy) parametric_consts;
+    val const_transfer_goals = map (mk_const_transfer_goal lthy'') parametric_consts;
 
     val rho_transfer_goal =
-      mk_rho_parametricity_goal lthy Y Z preT ssig_T dead_pre_rel dead_k_rel dead_ssig_rel rho_rhs;
+      mk_rho_parametricity_goal lthy'' Y Z preT ssig_T dead_pre_rel dead_k_rel dead_ssig_rel rho_rhs;
   in
-    ((rho_data, (const_transfer_goals, rho_transfer_goal)), lthy)
+    ((rho_data, (const_transfer_goals, rho_transfer_goal)), lthy'')
   end;
 
 fun explore_corec_equation ctxt could_be_friend friend fun_name fun_free
@@ -1814,12 +1814,12 @@
     fun pat_completeness_auto ctxt =
       Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt;
 
-    val ({defname, pelims = [[pelim]], pinducts = [pinduct], psimps = [psimp], ...}, lthy) =
+    val ({defname, pelims = [[pelim]], pinducts = [pinduct], psimps = [psimp], ...}, lthy') =
       Function.add_function [(Binding.concealed binding, NONE, NoSyn)]
         [(((Binding.concealed Binding.empty, []), parsed_eq), [], [])]
         Function_Common.default_config pat_completeness_auto lthy;
   in
-    ((defname, (pelim, pinduct, psimp)), lthy)
+    ((defname, (pelim, pinduct, psimp)), lthy')
   end;
 
 fun build_corecUU_arg_and_goals prove_termin (Free (fun_base_name, _)) (arg_ts, explored_rhs) lthy =
@@ -1983,48 +1983,48 @@
       (* FIXME: does this work with locales that fix variables? *)
 
     val no_base = has_no_corec_info lthy fpT_name;
-    val lthy = lthy |> no_base ? setup_base fpT_name;
+    val lthy1 = lthy |> no_base ? setup_base fpT_name;
 
-    fun extract_rho lthy =
+    fun extract_rho lthy' =
       let
-        val lthy = lthy |> Variable.declare_typ fun_T;
+        val lthy'' = lthy' |> Variable.declare_typ fun_T;
         val (prepared as (_, _, version, Y, Z, preT, k_T, ssig_T, dead_pre_bnf, dead_k_bnf, _,
-               ssig_fp_sugar, buffer), lthy) =
-          prepare_friend_corec fun_name fun_T lthy;
-        val friend_parse_info = friend_parse_info_of lthy arg_Ts res_T buffer;
+               ssig_fp_sugar, buffer), lthy''') =
+          prepare_friend_corec fun_name fun_T lthy'';
+        val friend_parse_info = friend_parse_info_of lthy''' arg_Ts res_T buffer;
 
         val parsed_eq' = parsed_eq ||> subst_atomic [(fun_free, fun_t)];
       in
-        lthy
+        lthy'''
         |> extract_rho_return_transfer_goals b version dead_pre_bnf dead_k_bnf Y Z preT k_T ssig_T
           ssig_fp_sugar friend_parse_info fun_t parsed_eq'
         |>> pair prepared
       end;
 
-    val ((prepareds, (rho_datas, transfer_goal_datas)), lthy) =
-      if friend then extract_rho lthy |>> (apfst single ##> (apfst single #> apsnd single))
-      else (([], ([], [])), lthy);
+    val ((prepareds, (rho_datas, transfer_goal_datas)), lthy2) =
+      if friend then extract_rho lthy1 |>> (apfst single ##> (apfst single #> apsnd single))
+      else (([], ([], [])), lthy1);
 
-    val ((buffer, corec_infos), lthy) =
+    val ((buffer, corec_infos), lthy3) =
       if friend then
-        ((#13 (the_single prepareds), []), lthy)
+        ((#13 (the_single prepareds), []), lthy2)
       else
-        corec_info_of res_T lthy
+        corec_info_of res_T lthy2
         ||> no_base ? update_coinduct_cong_intross_dynamic fpT_name
         |>> (fn info as {buffer, ...} => (buffer, [info]));
 
-    val corec_parse_info = corec_parse_info_of lthy arg_Ts res_T buffer;
+    val corec_parse_info = corec_parse_info_of lthy3 arg_Ts res_T buffer;
 
     val explored_eq =
-      explore_corec_equation lthy true friend fun_name fun_free corec_parse_info res_T parsed_eq;
+      explore_corec_equation lthy3 true friend fun_name fun_free corec_parse_info res_T parsed_eq;
 
-    val (((inner_fp_triple, termin_goals), corecUU_arg), lthy) =
-      build_corecUU_arg_and_goals (not long_cmd) fun_free explored_eq lthy;
+    val (((inner_fp_triple, termin_goals), corecUU_arg), lthy4) =
+      build_corecUU_arg_and_goals (not long_cmd) fun_free explored_eq lthy3;
 
     fun def_fun (inner_fp_elims0, inner_fp_inducts0, inner_fp_simps0) const_transfers
-        rho_transfers_foldeds lthy =
+        rho_transfers_foldeds lthy5 =
       let
-        fun register_friend lthy =
+        fun register_friend lthy' =
           let
             val [(old_corec_info, fp_b, version, Y, Z, _, k_T, _, _, dead_k_bnf, sig_fp_sugar,
                   ssig_fp_sugar, _)] = prepareds;
@@ -2035,53 +2035,53 @@
             val rho_transfer_folded =
               (case rho_transfers_foldeds of
                 [] =>
-                derive_rho_transfer_folded lthy fpT_name const_transfers rho_def rho_transfer_goal
+                derive_rho_transfer_folded lthy' fpT_name const_transfers rho_def rho_transfer_goal
               | [thm] => thm);
           in
-            lthy
+            lthy'
             |> register_coinduct_dynamic_friend fpT_name fun_name
             |> register_friend_corec fun_name fp_b version Y Z k_T dead_k_bnf sig_fp_sugar
               ssig_fp_sugar fun_t rho rho_transfer_folded old_corec_info
           end;
 
-        val (friend_infos, lthy) = lthy |> (if friend then register_friend #>> single else pair []);
-        val (corec_info as {corecUU = corecUU0, ...}, lthy) =
+        val (friend_infos, lthy6) = lthy5 |> (if friend then register_friend #>> single else pair []);
+        val (corec_info as {corecUU = corecUU0, ...}, lthy7) =
           (case corec_infos of
-            [] => corec_info_of res_T lthy
-          | [info] => (info, lthy));
+            [] => corec_info_of res_T lthy6
+          | [info] => (info, lthy6));
 
-        val def_rhs = mk_corec_fun_def_rhs lthy arg_Ts corecUU0 corecUU_arg;
+        val def_rhs = mk_corec_fun_def_rhs lthy7 arg_Ts corecUU0 corecUU_arg;
         val def = ((b, mx), ((Binding.concealed (Thm.def_binding b), []), def_rhs));
 
-        val ((fun_t0, (_, fun_def0)), (lthy, lthy_old)) = lthy
+        val ((fun_lhs0, (_, fun_def0)), (lthy9, lthy8')) = lthy7
           |> Local_Theory.open_target |> snd
           |> Local_Theory.define def
-          |> tap (fn (def, lthy) => print_def_consts int [def] lthy)
+          |> tap (fn (def, lthy') => print_def_consts int [def] lthy')
           ||> `Local_Theory.close_target;
 
-        val parsed_eq = parse_corec_equation lthy [fun_free] eq;
-        val views0 = generate_views lthy eq fun_free parsed_eq;
+        val parsed_eq = parse_corec_equation lthy9 [fun_free] eq;
+        val views0 = generate_views lthy9 eq fun_free parsed_eq;
 
-        val lthy' = lthy |> fold Variable.declare_typ (res_T :: arg_Ts);
-        val phi = Proof_Context.export_morphism lthy_old lthy';
+        val lthy9' = lthy9 |> fold Variable.declare_typ (res_T :: arg_Ts);
+        val phi = Proof_Context.export_morphism lthy8' lthy9';
 
-        val fun_t = Morphism.term phi fun_t0; (* FIXME: shadows "fun_t" -- identical? *)
+        val fun_lhs = Morphism.term phi fun_lhs0;
         val fun_def = Morphism.thm phi fun_def0;
         val inner_fp_elims = map (Morphism.thm phi) inner_fp_elims0;
         val inner_fp_inducts = map (Morphism.thm phi) inner_fp_inducts0;
         val inner_fp_simps = map (Morphism.thm phi) inner_fp_simps0;
         val (code_goal, _, _, _, _) = morph_views phi views0;
 
-        fun derive_and_note_friend_extra_theorems lthy =
+        fun derive_and_note_friend_extra_theorems lthy' =
           let
             val k_T = #7 (the_single prepareds);
             val rho_def = snd (the_single rho_datas);
 
-            val (eq_algrho, algrho_eq) = derive_eq_algrho lthy corec_info (the_single friend_infos)
-              fun_t k_T code_goal const_transfers rho_def fun_def;
+            val (eq_algrho, algrho_eq) = derive_eq_algrho lthy' corec_info (the_single friend_infos)
+              fun_lhs k_T code_goal const_transfers rho_def fun_def;
 
             val notes =
-              (if Config.get lthy bnf_internals then
+              (if Config.get lthy' bnf_internals then
                  [(eq_algrhoN, [eq_algrho])]
                else
                  [])
@@ -2090,14 +2090,14 @@
                     (Binding.qualify false friendN (Binding.name thmN)), []),
                  [(thms, [])]));
           in
-            lthy
+            lthy'
             |> register_friend_extra fun_name eq_algrho algrho_eq
             |> Local_Theory.notes notes |> snd
           end;
 
-        val lthy = lthy |> friend ? derive_and_note_friend_extra_theorems;
+        val lthy10 = lthy9 |> friend ? derive_and_note_friend_extra_theorems;
 
-        val code_thm = derive_code lthy inner_fp_simps code_goal corec_info fun_t fun_def;
+        val code_thm = derive_code lthy10 inner_fp_simps code_goal corec_info fun_lhs fun_def;
 (* TODO:
         val ctr_thmss = map mk_thm (#2 views);
         val disc_thmss = map mk_thm (#3 views);
@@ -2107,7 +2107,7 @@
 
         val uniques =
           if null inner_fp_simps then
-            [derive_unique lthy phi (#1 views0) corec_info fpT_name fun_def]
+            [derive_unique lthy10 phi (#1 views0) corec_info fpT_name fun_def]
           else
             [];
 
@@ -2117,7 +2117,7 @@
         val simp_thmss = map2 append disc_iff_or_disc_thmss sel_thmss;
 *)
 
-        val ((_, [{cong_intro_pairs, coinduct, coinduct_attrs}]), lthy) = lthy
+        val ((_, [{cong_intro_pairs, coinduct, coinduct_attrs}]), lthy11) = lthy10
           |> derive_and_update_coinduct_cong_intross [corec_info];
         val cong_intros_pairs = AList.group (op =) cong_intro_pairs;
 
@@ -2134,7 +2134,7 @@
            (inner_inductN, inner_fp_inducts, []),
            (uniqueN, uniques, [])] @
            map (fn (thmN, thms) => (thmN, thms, [])) cong_intros_pairs @
-          (if Config.get lthy bnf_internals then
+          (if Config.get lthy11 bnf_internals then
              [(inner_elimN, inner_fp_elims, []),
               (inner_simpN, inner_fp_simps, [])]
            else
@@ -2152,12 +2152,12 @@
                [(thms, [])]))
           |> filter_out (null o fst o hd o snd);
       in
-        lthy
+        lthy11
 (* TODO:
-        |> 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_lhs], flat sel_thmss)
+        |> Spec_Rules.add Spec_Rules.equational ([fun_lhs], flat ctr_thmss)
 *)
-        |> Spec_Rules.add "" Spec_Rules.equational [fun_t0] [code_thm]
+        |> Spec_Rules.add Binding.empty Spec_Rules.equational [fun_lhs] [code_thm]
         |> plugins code_plugin ? Code.declare_default_eqns [(code_thm, true)]
         |> Local_Theory.notes (anonymous_notes @ notes)
         |> snd
@@ -2177,16 +2177,16 @@
     val const_transfer_goals = fold (union (op aconv) o fst) transfer_goal_datas [];
     val (const_transfers, const_transfer_goals') =
       if long_cmd then ([], const_transfer_goals)
-      else fold (maybe_prove_transfer_goal lthy) const_transfer_goals ([], []);
+      else fold (maybe_prove_transfer_goal lthy4) const_transfer_goals ([], []);
   in
     ((def_fun, (([res_T], prepareds, rho_datas, map snd transfer_goal_datas),
-        (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals'))), lthy)
+        (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals'))), lthy4)
   end;
 
 fun corec_cmd int opts (raw_fixes, raw_eq) lthy =
   let
     val ((def_fun, (_, (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals))),
-         lthy) =
+         lthy') =
       prepare_corec_ursive_cmd int false opts (raw_fixes, raw_eq) lthy;
   in
     if not (null termin_goals) then
@@ -2196,32 +2196,32 @@
       error ("Transfer prover failed (try " ^ quote (#1 \<^command_keyword>\<open>corecursive\<close>) ^
         " instead of " ^ quote (#1 \<^command_keyword>\<open>corec\<close>) ^ ")")
     else
-      def_fun inner_fp_triple const_transfers [] lthy
+      def_fun inner_fp_triple const_transfers [] lthy'
   end;
 
 fun corecursive_cmd int opts (raw_fixes, raw_eq) lthy =
   let
     val ((def_fun, (([Type (fpT_name, _)], prepareds, rho_datas, rho_transfer_goals),
-            (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals))), lthy) =
+            (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals))), lthy') =
       prepare_corec_ursive_cmd int true opts (raw_fixes, raw_eq) lthy;
 
     val (rho_transfer_goals', unprime_rho_transfer_and_folds) =
       @{map 3} (fn (_, _, _, _, _, _, _, _, _, _, _, _, _) => fn (_, rho_def) =>
-          prime_rho_transfer_goal lthy fpT_name rho_def)
+          prime_rho_transfer_goal lthy' fpT_name rho_def)
         prepareds rho_datas rho_transfer_goals
       |> split_list;
   in
     Proof.theorem NONE (fn [termin_thms, const_transfers', rho_transfers'] =>
       let
         val remove_domain_condition =
-          full_simplify (put_simpset HOL_basic_ss lthy
+          full_simplify (put_simpset HOL_basic_ss lthy'
             addsimps (@{thm True_implies_equals} :: termin_thms));
       in
         def_fun (@{apply 3} (map remove_domain_condition) inner_fp_triple)
           (const_transfers @ const_transfers')
           (map2 (fn f => f) unprime_rho_transfer_and_folds rho_transfers')
       end)
-      (map (map (rpair [])) [termin_goals, const_transfer_goals, rho_transfer_goals']) lthy
+      (map (map (rpair [])) [termin_goals, const_transfer_goals, rho_transfer_goals']) lthy'
   end;
 
 fun friend_of_corec_cmd ((raw_fun_name, raw_fun_T_opt), raw_eq) lthy =
@@ -2248,24 +2248,24 @@
     val (arg_Ts, res_T as Type (fpT_name, _)) = strip_type fun_T;
 
     val no_base = has_no_corec_info lthy fpT_name;
-    val lthy = lthy |> no_base ? setup_base fpT_name;
+    val lthy1 = lthy |> no_base ? setup_base fpT_name;
 
-    val lthy = lthy |> Variable.declare_typ fun_T;
+    val lthy2 = lthy1 |> Variable.declare_typ fun_T;
     val ((old_corec_info, fp_b, version, Y, Z, preT, k_T, ssig_T, dead_pre_bnf, dead_k_bnf,
-          sig_fp_sugar, ssig_fp_sugar, buffer), lthy) =
-      prepare_friend_corec fun_name fun_T lthy;
-    val friend_parse_info = friend_parse_info_of lthy arg_Ts res_T buffer;
+          sig_fp_sugar, ssig_fp_sugar, buffer), lthy3) =
+      prepare_friend_corec fun_name fun_T lthy2;
+    val friend_parse_info = friend_parse_info_of lthy3 arg_Ts res_T buffer;
 
-    val parsed_eq = parse_corec_equation lthy [] code_goal;
+    val parsed_eq = parse_corec_equation lthy3 [] code_goal;
 
-    val (((rho, rho_def), (const_transfer_goals, rho_transfer_goal)), lthy) =
+    val (((rho, rho_def), (const_transfer_goals, rho_transfer_goal)), lthy4) =
       extract_rho_return_transfer_goals fun_b version dead_pre_bnf dead_k_bnf Y Z preT k_T ssig_T
-        ssig_fp_sugar friend_parse_info fun_t parsed_eq lthy;
+        ssig_fp_sugar friend_parse_info fun_t parsed_eq lthy3;
 
     fun register_friend_extra_and_note_thms code_goal code_thm const_transfers k_T friend_info
-        lthy =
+        lthy5 =
       let
-        val (corec_info, lthy) = corec_info_of res_T lthy;
+        val (corec_info, lthy6) = corec_info_of res_T lthy5;
 
         val fun_free = Free (Binding.name_of fun_b, fun_T);
 
@@ -2273,25 +2273,25 @@
           | freeze_fun t = t;
 
         val eq = Term.map_aterms freeze_fun code_goal;
-        val parsed_eq = parse_corec_equation lthy [fun_free] eq;
+        val parsed_eq = parse_corec_equation lthy6 [fun_free] eq;
 
-        val corec_parse_info = corec_parse_info_of lthy arg_Ts res_T buffer;
-        val explored_eq = explore_corec_equation lthy false false fun_name fun_free corec_parse_info
+        val corec_parse_info = corec_parse_info_of lthy6 arg_Ts res_T buffer;
+        val explored_eq = explore_corec_equation lthy6 false false fun_name fun_free corec_parse_info
           res_T parsed_eq;
 
-        val ((_, corecUU_arg), _) = build_corecUU_arg_and_goals false fun_free explored_eq lthy;
+        val ((_, corecUU_arg), _) = build_corecUU_arg_and_goals false fun_free explored_eq lthy6;
 
-        val eq_corecUU = derive_eq_corecUU lthy corec_info fun_t corecUU_arg code_thm;
-        val (eq_algrho, algrho_eq) = derive_eq_algrho lthy corec_info friend_info fun_t k_T
+        val eq_corecUU = derive_eq_corecUU lthy6 corec_info fun_t corecUU_arg code_thm;
+        val (eq_algrho, algrho_eq) = derive_eq_algrho lthy6 corec_info friend_info fun_t k_T
           code_goal const_transfers rho_def eq_corecUU;
 
-        val ((_, [{cong_intro_pairs, coinduct, coinduct_attrs}]), lthy) = lthy
+        val ((_, [{cong_intro_pairs, coinduct, coinduct_attrs}]), lthy7) = lthy6
           |> register_friend_extra fun_name eq_algrho algrho_eq
           |> register_coinduct_dynamic_friend fpT_name fun_name
           |> derive_and_update_coinduct_cong_intross [corec_info];
         val cong_intros_pairs = AList.group (op =) cong_intro_pairs;
 
-        val unique = derive_unique lthy Morphism.identity code_goal corec_info fpT_name eq_corecUU;
+        val unique = derive_unique lthy7 Morphism.identity code_goal corec_info fpT_name eq_corecUU;
 
         val notes =
           [(codeN, [code_thm], []),
@@ -2299,7 +2299,7 @@
            (cong_introsN, maps snd cong_intros_pairs, []),
            (uniqueN, [unique], [])] @
            map (fn (thmN, thms) => (thmN, thms, [])) cong_intros_pairs @
-          (if Config.get lthy bnf_internals then
+          (if Config.get lthy7 bnf_internals then
              [(eq_algrhoN, [eq_algrho], []),
               (eq_corecUUN, [eq_corecUU], [])]
            else
@@ -2309,14 +2309,14 @@
                 (Binding.qualify false friendN (Binding.name thmN)), attrs),
              [(thms, [])]));
       in
-        lthy
+        lthy7
         |> Local_Theory.notes notes |> snd
       end;
 
     val (rho_transfer_goal', unprime_rho_transfer_and_fold) =
-      prime_rho_transfer_goal lthy fpT_name rho_def rho_transfer_goal;
+      prime_rho_transfer_goal lthy4 fpT_name rho_def rho_transfer_goal;
   in
-    lthy
+    lthy4
     |> Proof.theorem NONE (fn [[code_thm], const_transfers, [rho_transfer']] =>
         register_friend_corec fun_name fp_b version Y Z k_T dead_k_bnf sig_fp_sugar ssig_fp_sugar
           fun_t rho (unprime_rho_transfer_and_fold rho_transfer') old_corec_info
@@ -2331,13 +2331,13 @@
 
     val no_base = has_no_corec_info lthy fpT_name;
 
-    val (corec_info as {version, ...}, lthy) = lthy
+    val (corec_info as {version, ...}, lthy1) = lthy
       |> corec_info_of fpT;
-    val lthy = lthy |> no_base ? setup_base fpT_name;
+    val lthy2 = lthy1 |> no_base ? setup_base fpT_name;
 
-    val ((changed, [{cong_intro_pairs, coinduct, coinduct_attrs}]), lthy) = lthy
+    val ((changed, [{cong_intro_pairs, coinduct, coinduct_attrs}]), lthy3) = lthy2
       |> derive_and_update_coinduct_cong_intross [corec_info];
-    val lthy = lthy |> (changed orelse no_base) ? update_coinduct_cong_intross_dynamic fpT_name;
+    val lthy4 = lthy3 |> (changed orelse no_base) ? update_coinduct_cong_intross_dynamic fpT_name;
     val cong_intros_pairs = AList.group (op =) cong_intro_pairs;
 
     val notes =
@@ -2349,16 +2349,16 @@
             (Binding.qualify false ("v" ^ string_of_int version) (Binding.name thmN))), attrs),
          [(thms, [])]));
   in
-    lthy |> Local_Theory.notes notes |> snd
+    lthy4 |> Local_Theory.notes notes |> snd
   end;
 
 fun consolidate lthy =
   let
     val corec_infoss = map (corec_infos_of lthy o fst) (all_codatatype_extras_of lthy);
-    val (changeds, lthy) = lthy
+    val (changeds, lthy') = lthy
       |> fold_map (apfst fst oo derive_and_update_coinduct_cong_intross) corec_infoss;
   in
-    if exists I changeds then lthy else raise Same.SAME
+    if exists I changeds then lthy' else raise Same.SAME
   end;
 
 fun consolidate_global thy =
diff -r 6617fb368a06 -r 35e465677a26 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Dec 03 15:20:30 2019 +0100
@@ -1533,9 +1533,10 @@
         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 Binding.empty (Spec_Rules.equational_primcorec primcorec_types)
+            fun_ts0 (flat sel_thmss)
+        |> Spec_Rules.add Binding.empty Spec_Rules.equational fun_ts0 (flat ctr_thmss)
+        |> Spec_Rules.add Binding.empty 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 6617fb368a06 -r 35e465677a26 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Dec 03 15:20:30 2019 +0100
@@ -637,7 +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 spec_name = Binding.conglomerate (map (#1 o #1) fixes);
 
     val mk_notes =
       flat oooo @{map 4} (fn js => fn prefix => fn qualify => fn thms =>
diff -r 6617fb368a06 -r 35e465677a26 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Dec 03 15:20:30 2019 +0100
@@ -373,8 +373,9 @@
 
       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 Binding.empty Spec_Rules.equational size_consts size_simps
+        |> Spec_Rules.add Binding.empty 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 6617fb368a06 -r 35e465677a26 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Dec 03 15:20:30 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 (uncurry (Spec_Rules.add "" Spec_Rules.equational))
+          |> Spec_Rules.add Binding.empty Spec_Rules.equational [casex] case_thms
+          |> fold (uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational))
             (AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms))
-          |> fold (uncurry (Spec_Rules.add "" Spec_Rules.equational))
+          |> fold (uncurry (Spec_Rules.add Binding.empty 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 6617fb368a06 -r 35e465677a26 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/Function/function.ML	Tue Dec 03 15:20:30 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 Binding.empty Spec_Rules.equational_recdef fs tsimps)
           end)
       end
   in
diff -r 6617fb368a06 -r 35e465677a26 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Dec 03 15:20:30 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 Binding.empty 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 6617fb368a06 -r 35e465677a26 src/HOL/Tools/Nunchaku/nunchaku_collect.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Tue Dec 03 15:20:30 2019 +0100
@@ -500,7 +500,7 @@
 
     val specs =
       if s = \<^const_name>\<open>The\<close> then
-        [{name = "", rough_classification = Spec_Rules.Unknown,
+        [{pos = Position.none, 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
@@ -508,7 +508,7 @@
           if card = Inf orelse card = Fin_or_Inf then
             spec_rules ()
           else
-            [{name = "", rough_classification = Spec_Rules.equational,
+            [{pos = Position.none, 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
diff -r 6617fb368a06 -r 35e465677a26 src/HOL/Tools/Old_Datatype/old_primrec.ML
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Tue Dec 03 15:20:30 2019 +0100
@@ -278,7 +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));
+    val spec_name = 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 =
diff -r 6617fb368a06 -r 35e465677a26 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/inductive.ML	Tue Dec 03 15:20:30 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 -> string list -> term list ->
+  val declare_rules: binding -> bool -> bool -> binding -> 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
@@ -1099,7 +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 spec_name = 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));
diff -r 6617fb368a06 -r 35e465677a26 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Tue Dec 03 15:20:30 2019 +0100
@@ -503,7 +503,7 @@
     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 spec_name = 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) =
diff -r 6617fb368a06 -r 35e465677a26 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/record.ML	Tue Dec 03 15:20:30 2019 +0100
@@ -1814,7 +1814,7 @@
 
 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;
+  in Spec_Rules.add_global Binding.empty Spec_Rules.equational [head] [rule] end;
 
 (* definition *)
 
diff -r 6617fb368a06 -r 35e465677a26 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/Pure/General/binding.ML	Tue Dec 03 15:20:30 2019 +0100
@@ -122,7 +122,7 @@
 fun is_empty_atts (b, atts) = is_empty b andalso null atts;
 
 fun conglomerate [b] = b
-  | conglomerate bs = name (space_implode "_" (map name_of bs));
+  | conglomerate bs = name (space_implode "_" (map name_of (filter_out is_empty bs)));
 
 
 (* user qualifier *)
diff -r 6617fb368a06 -r 35e465677a26 src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/Pure/Isar/spec_rules.ML	Tue Dec 03 15:20:30 2019 +0100
@@ -1,7 +1,9 @@
 (*  Title:      Pure/Isar/spec_rules.ML
     Author:     Makarius
 
-Rules that characterize specifications, with rough classification.
+Rules that characterize specifications, with optional name and
+rough classification.
+
 NB: In the face of arbitrary morphisms, the original shape of
 specifications may get lost.
 *)
@@ -11,6 +13,7 @@
   datatype recursion =
     Primrec of string list | Recdef | Primcorec of string list | Corec | Unknown_Recursion
   val recursion_ord: recursion ord
+  val encode_recursion: recursion XML.Encode.T
   datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown
   val rough_classification_ord: rough_classification ord
   val equational_primrec: string list -> rough_classification
@@ -23,14 +26,20 @@
   val is_co_inductive: rough_classification -> bool
   val is_relational: rough_classification -> bool
   val is_unknown: rough_classification -> bool
-  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: string -> rough_classification -> term list -> thm list -> local_theory -> local_theory
-  val add_global: string -> rough_classification -> term list -> thm list -> theory -> theory
+  val encode_rough_classification: rough_classification XML.Encode.T
+  type spec_rule =
+   {pos: Position.T,
+    name: string,
+    rough_classification: rough_classification,
+    terms: term list,
+    rules: thm list}
+  val get: Proof.context -> spec_rule list
+  val get_global: theory -> spec_rule list
+  val dest_theory: theory -> spec_rule list
+  val retrieve: Proof.context -> term -> spec_rule list
+  val retrieve_global: theory -> term -> spec_rule list
+  val add: binding -> rough_classification -> term list -> thm list -> local_theory -> local_theory
+  val add_global: binding -> rough_classification -> term list -> thm list -> theory -> theory
 end;
 
 structure Spec_Rules: SPEC_RULES =
@@ -48,6 +57,16 @@
   | recursion_ord (Primcorec Ts1, Primcorec Ts2) = list_ord fast_string_ord (Ts1, Ts2)
   | recursion_ord rs = int_ord (apply2 recursion_index rs);
 
+val encode_recursion =
+  let open XML.Encode in
+    variant
+     [fn Primrec a => ([], list string a),
+      fn Recdef => ([], []),
+      fn Primcorec a => ([], list string a),
+      fn Corec => ([], []),
+      fn Unknown_Recursion => ([], [])]
+  end;
+
 
 (* rough classification *)
 
@@ -69,24 +88,38 @@
 val is_relational = is_inductive orf is_co_inductive;
 val is_unknown = fn Unknown => true | _ => false;
 
+val encode_rough_classification =
+  let open XML.Encode in
+    variant
+     [fn Equational r => ([], encode_recursion r),
+      fn Inductive => ([], []),
+      fn Co_Inductive => ([], []),
+      fn Unknown => ([], [])]
+  end;
+
 
 (* rules *)
 
-type spec =
-  {name: string, rough_classification: rough_classification, terms: term list, rules: thm list};
+type spec_rule =
+ {pos: Position.T,
+  name: string,
+  rough_classification: rough_classification,
+  terms: term list,
+  rules: thm list};
 
-fun eq_spec (specs: spec * spec) =
+fun eq_spec (specs: spec_rule * spec_rule) =
   (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};
+fun map_spec_rules f ({pos, name, rough_classification, terms, rules}: spec_rule) : spec_rule =
+  {pos = pos, name = name, rough_classification = rough_classification, terms = terms,
+    rules = map f rules};
 
 structure Rules = Generic_Data
 (
-  type T = spec Item_Net.T;
+  type T = spec_rule Item_Net.T;
   val empty : T = Item_Net.init eq_spec #terms;
   val extend = I;
   val merge = Item_Net.merge;
@@ -95,17 +128,22 @@
 
 (* get *)
 
-fun get_generic context =
+fun get_generic imports context =
   let
     val thy = Context.theory_of context;
     val transfer = Global_Theory.transfer_theories thy;
+    fun imported spec =
+      imports |> exists (fn thy => Item_Net.member (Rules.get (Context.Theory thy)) spec);
   in
     Item_Net.content (Rules.get context)
+    |> filter_out imported
     |> (map o map_spec_rules) transfer
   end;
 
-val get = get_generic o Context.Proof;
-val get_global = get_generic o Context.Theory;
+val get = get_generic [] o Context.Proof;
+val get_global = get_generic [] o Context.Theory;
+
+fun dest_theory thy = rev (get_generic (Theory.parents_of thy) (Context.Theory thy));
 
 
 (* retrieve *)
@@ -120,11 +158,13 @@
 
 (* add *)
 
-fun add name rough_classification terms rules lthy =
+fun add b 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 context =>
         let
+          val pos = Position.thread_data ();
+          val name = Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding phi b);
           val (terms', rules') =
             map (Thm.transfer (Context.theory_of context)) thms0
             |> Morphism.fact phi
@@ -133,14 +173,17 @@
             ||> map Thm.trim_context;
         in
           context |> (Rules.map o Item_Net.update)
-            {name = name, rough_classification = rough_classification,
+            {pos = pos, name = name, rough_classification = rough_classification,
               terms = terms', rules = rules'}
         end)
   end;
 
-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};
+fun add_global b rough_classification terms rules thy =
+  thy |> (Context.theory_map o Rules.map o Item_Net.update)
+   {pos = Position.thread_data (),
+    name = Sign.full_name thy b,
+    rough_classification = rough_classification,
+    terms = terms,
+    rules = map Thm.trim_context rules};
 
 end;
diff -r 6617fb368a06 -r 35e465677a26 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Dec 03 15:20:30 2019 +0100
@@ -216,6 +216,10 @@
     val specs =
       map ((apsnd o map) (prep_att vars_ctxt) o fst) raw_concls ~~ map close concls;
 
+    val spec_name =
+      Binding.conglomerate (if null decls then map (#1 o #1) specs else map (#1 o #1) decls);
+
+
     (*consts*)
     val (consts, consts_thy) = thy
       |> fold_map (fn ((b, _, mx), (_, t)) => Theory.specify_const ((b, Term.type_of t), mx)) decls;
@@ -229,7 +233,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_name 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;
@@ -265,7 +269,7 @@
       |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
 
     val th = prove lthy2 raw_th;
-    val lthy3 = lthy2 |> Spec_Rules.add const_name Spec_Rules.equational [lhs] [th];
+    val lthy3 = lthy2 |> Spec_Rules.add name Spec_Rules.equational [lhs] [th];
 
     val ([(def_name, [th'])], lthy4) = lthy3
       |> Local_Theory.notes [((name, atts), [([th], [])])];
diff -r 6617fb368a06 -r 35e465677a26 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/Pure/Proof/extraction.ML	Tue Dec 03 15:20:30 2019 +0100
@@ -816,7 +816,6 @@
         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 [(b, fastype_of ft, NoSyn)]
@@ -824,7 +823,8 @@
            [((Binding.qualified_name (Thm.def_name (extr_name s vs)),
              Logic.mk_equals (head, ft)), [])]
         |-> (fn [def_thm] =>
-           Spec_Rules.add_global const_name Spec_Rules.equational [head] [def_thm]
+           Spec_Rules.add_global b Spec_Rules.equational
+             [Thm.term_of (Thm.lhs_of def_thm)] [def_thm]
            #> Code.declare_default_eqns_global [(def_thm, true)])
       end;
 
diff -r 6617fb368a06 -r 35e465677a26 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Tue Dec 03 15:20:30 2019 +0100
@@ -67,7 +67,7 @@
   |> the_default ([], false);
 
 
-(* locales content *)
+(* locales *)
 
 fun locale_content thy loc =
   let
@@ -141,14 +141,32 @@
     val thy_ctxt = Proof_Context.init_global thy;
 
 
+    (* spec rules *)
+
+    fun position_properties pos =
+      Position.offset_properties_of (adjust_pos pos) @ Position.id_properties_of pos;
+
+    fun spec_rule_content {pos, name, rough_classification, terms, rules} =
+      let
+        val spec =
+          terms @ map Thm.plain_prop_of rules
+          |> Term_Subst.zero_var_indexes_list
+          |> map Logic.unvarify_global;
+      in
+       {props = position_properties pos,
+        name = name,
+        rough_classification = rough_classification,
+        typargs = rev (fold Term.add_tfrees spec []),
+        args = rev (fold Term.add_frees spec []),
+        terms = map (fn t => (t, Term.type_of t)) (take (length terms) spec),
+        rules = drop (length terms) spec}
+      end;
+
+
     (* entities *)
 
     fun make_entity_markup name xname pos serial =
-      let
-        val props =
-          Position.offset_properties_of (adjust_pos pos) @
-          Position.id_properties_of pos @
-          Markup.serial_properties serial;
+      let val props = position_properties pos @ Markup.serial_properties serial;
       in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end;
 
     fun entity_markup space name =
@@ -232,6 +250,9 @@
         val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
       in ((sorts @ typargs, args, prop), proof) end;
 
+    fun standard_prop_of thm =
+      standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm);
+
     val encode_prop =
       let open XML.Encode Term_XML.Encode
       in triple (list (pair string sort)) (list (pair string typ)) encode_term end;
@@ -247,6 +268,7 @@
     (* theorems and proof terms *)
 
     val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps;
+    val prep_thm = clean_thm #> Thm.unconstrainT;
 
     val lookup_thm_id = Global_Theory.lookup_thm_id thy;
 
@@ -267,7 +289,7 @@
     fun encode_thm thm_id raw_thm =
       let
         val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
-        val thm = clean_thm (Thm.unconstrainT raw_thm);
+        val thm = prep_thm raw_thm;
 
         val proof0 =
           if Proofterm.export_standard_enabled () then
@@ -275,8 +297,7 @@
               {full = true, expand_name = SOME o expand_name thm_id} thm
           else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm
           else MinProof;
-        val (prop, SOME proof) =
-          standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0);
+        val (prop, SOME proof) = standard_prop_of thm (SOME proof0);
         val _ = Thm.expose_proofs thy [thm];
       in
         (prop, deps, proof) |>
@@ -397,6 +418,23 @@
       if null constdefs then () else export_body thy "constdefs" (encode_constdefs constdefs);
 
 
+    (* spec rules *)
+
+    val encode_specs =
+      let open XML.Encode Term_XML.Encode in
+        list (fn {props, name, rough_classification, typargs, args, terms, rules} =>
+          pair properties (pair string (pair Spec_Rules.encode_rough_classification
+            (pair (list (pair string sort)) (pair (list (pair string typ))
+              (pair (list (pair encode_term typ)) (list encode_term))))))
+              (props, (name, (rough_classification, (typargs, (args, (terms, rules)))))))
+      end;
+
+    val _ =
+      (case Spec_Rules.dest_theory thy of
+        [] => ()
+      | spec_rules => export_body thy "spec_rules" (encode_specs (map spec_rule_content spec_rules)));
+
+
     (* parents *)
 
     val _ =
diff -r 6617fb368a06 -r 35e465677a26 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Mon Dec 02 17:51:54 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala	Tue Dec 03 15:20:30 2019 +0100
@@ -42,6 +42,7 @@
     arities: Boolean = true,
     constdefs: Boolean = true,
     typedefs: Boolean = true,
+    spec_rules: Boolean = true,
     cache: Term.Cache = Term.make_cache()): Session =
   {
     val thys =
@@ -56,7 +57,8 @@
                 session, theory, types = types, consts = consts,
                 axioms = axioms, thms = thms, classes = classes, locales = locales,
                 locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
-                constdefs = constdefs, typedefs = typedefs, cache = Some(cache))
+                constdefs = constdefs, typedefs = typedefs,
+                spec_rules = spec_rules, cache = Some(cache))
             }
           }
         }))
@@ -90,7 +92,8 @@
     classrel: List[Classrel],
     arities: List[Arity],
     constdefs: List[Constdef],
-    typedefs: List[Typedef])
+    typedefs: List[Typedef],
+    spec_rules: List[Spec_Rule])
   {
     override def toString: String = name
 
@@ -116,7 +119,8 @@
         classrel.map(_.cache(cache)),
         arities.map(_.cache(cache)),
         constdefs.map(_.cache(cache)),
-        typedefs.map(_.cache(cache)))
+        typedefs.map(_.cache(cache)),
+        spec_rules.map(_.cache(cache)))
   }
 
   def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
@@ -131,6 +135,7 @@
     arities: Boolean = true,
     constdefs: Boolean = true,
     typedefs: Boolean = true,
+    spec_rules: Boolean = true,
     cache: Option[Term.Cache] = None): Theory =
   {
     val parents =
@@ -155,7 +160,8 @@
         if (classrel) read_classrel(provider) else Nil,
         if (arities) read_arities(provider) else Nil,
         if (constdefs) read_constdefs(provider) else Nil,
-        if (typedefs) read_typedefs(provider) else Nil)
+        if (typedefs) read_typedefs(provider) else Nil,
+        if (spec_rules) read_spec_rules(provider) else Nil)
     if (cache.isDefined) theory.cache(cache.get) else theory
   }
 
@@ -643,4 +649,102 @@
     for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
     yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
   }
+
+
+  /* Pure spec rules */
+
+  sealed abstract class Recursion
+  {
+    def cache(cache: Term.Cache): Recursion =
+      this match {
+        case Primrec(types) => Primrec(types.map(cache.string))
+        case Primcorec(types) => Primcorec(types.map(cache.string))
+        case _ => this
+      }
+  }
+  case class Primrec(types: List[String]) extends Recursion
+  case object Recdef extends Recursion
+  case class Primcorec(types: List[String]) extends Recursion
+  case object Corec extends Recursion
+  case object Unknown_Recursion extends Recursion
+
+  val decode_recursion: XML.Decode.T[Recursion] =
+  {
+    import XML.Decode._
+    variant(List(
+      { case (Nil, a) => Primrec(list(string)(a)) },
+      { case (Nil, Nil) => Recdef },
+      { case (Nil, a) => Primcorec(list(string)(a)) },
+      { case (Nil, Nil) => Corec },
+      { case (Nil, Nil) => Unknown_Recursion }))
+  }
+
+
+  sealed abstract class Rough_Classification
+  {
+    def is_equational: Boolean = this.isInstanceOf[Equational]
+    def is_inductive: Boolean = this == Inductive
+    def is_co_inductive: Boolean = this == Co_Inductive
+    def is_relational: Boolean = is_inductive || is_co_inductive
+    def is_unknown: Boolean = this == Unknown
+
+    def cache(cache: Term.Cache): Rough_Classification =
+      this match {
+        case Equational(recursion) => Equational(recursion.cache(cache))
+        case _ => this
+      }
+  }
+  case class Equational(recursion: Recursion) extends Rough_Classification
+  case object Inductive extends Rough_Classification
+  case object Co_Inductive extends Rough_Classification
+  case object Unknown extends Rough_Classification
+
+  val decode_rough_classification: XML.Decode.T[Rough_Classification] =
+  {
+    import XML.Decode._
+    variant(List(
+      { case (Nil, a) => Equational(decode_recursion(a)) },
+      { case (Nil, Nil) => Inductive },
+      { case (Nil, Nil) => Co_Inductive },
+      { case (Nil, Nil) => Unknown }))
+  }
+
+
+  sealed case class Spec_Rule(
+    pos: Position.T,
+    name: String,
+    rough_classification: Rough_Classification,
+    typargs: List[(String, Term.Sort)],
+    args: List[(String, Term.Typ)],
+    terms: List[(Term.Term, Term.Typ)],
+    rules: List[Term.Term])
+  {
+    def id: Option[Long] = Position.Id.unapply(pos)
+
+    def cache(cache: Term.Cache): Spec_Rule =
+      Spec_Rule(
+        cache.position(pos),
+        cache.string(name),
+        rough_classification.cache(cache),
+        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
+        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
+        terms.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }),
+        rules.map(cache.term(_)))
+  }
+
+  def read_spec_rules(provider: Export.Provider): List[Spec_Rule] =
+  {
+    val body = provider.uncompressed_yxml(export_prefix + "spec_rules")
+    val spec_rules =
+    {
+      import XML.Decode._
+      import Term_XML.Decode._
+      list(
+        pair(properties, pair(string, pair(decode_rough_classification,
+          pair(list(pair(string, sort)), pair(list(pair(string, typ)),
+            pair(list(pair(term, typ)), list(term))))))))(body)
+    }
+    for ((pos, (name, (rough_classification, (typargs, (args, (terms, rules)))))) <- spec_rules)
+      yield Spec_Rule(pos, name, rough_classification, typargs, args, terms, rules)
+  }
 }