# HG changeset patch
# User wenzelm
# Date 1553634816 -3600
# Node ID bd3c10813cc452b51316590eea3101f8de8277c4
# Parent  6b097aeb3650c06f313cbb09371b9067d3b680ee
more informative Spec_Rules.Equational, notably primrec argument types;

diff -r 6b097aeb3650 -r bd3c10813cc4 src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/HOL/Library/old_recdef.ML	Tue Mar 26 22:13:36 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 ([lhs], flat rules)
+      ||> Spec_Rules.add_global 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 6b097aeb3650 -r bd3c10813cc4 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 26 22:13:36 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)
+          |> 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)
+            ? 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)
           |> 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 (curry (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 6b097aeb3650 -r bd3c10813cc4 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Mar 26 22:13:36 2019 +0100
@@ -2154,10 +2154,10 @@
       in
         lthy
 (* 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_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 6b097aeb3650 -r bd3c10813cc4 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 26 22:13:36 2019 +0100
@@ -1532,9 +1532,9 @@
         val fun_ts0 = map fst def_infos;
       in
         lthy
-        |> Spec_Rules.add Spec_Rules.Equational (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 (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 6b097aeb3650 -r bd3c10813cc4 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Mar 26 22:13:36 2019 +0100
@@ -580,7 +580,7 @@
         ((common_qualify (Binding.qualify true common_name (Binding.name thmN)), attrs),
           [(thms, [])]));
   in
-    (((fun_names, qualifys, defs),
+    (((fun_names, qualifys, arg_Ts, defs),
       fn lthy => fn defs =>
         let
           val def_thms = map (snd o snd) defs;
@@ -605,24 +605,29 @@
     val nonexhaustives = replicate actual_nn nonexhaustive;
     val transfers = replicate actual_nn transfer;
 
-    val (((names, qualifys, defs), prove), lthy') =
+    val (((names, qualifys, arg_Ts, defs), prove), lthy') =
       prepare_primrec plugins nonexhaustives transfers fixes ts lthy;
   in
     lthy'
     |> fold_map Local_Theory.define defs
     |> tap (uncurry (print_def_consts int))
     |-> (fn defs => fn lthy =>
-      let val ((jss, simpss), lthy) = prove lthy defs in
-        (((names, qualifys), (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy)
-      end)
+      let
+        val ((jss, simpss), lthy) = prove lthy defs;
+        val res =
+          {prefix = (names, qualifys),
+           types = map (#1 o dest_Type) arg_Ts,
+           result = (map fst defs, map (snd o snd) defs, (jss, simpss))};
+      in (res, lthy) end)
   end;
 
 fun primrec_simple int fixes ts lthy =
   primrec_simple0 int Plugin_Name.default_filter false false fixes ts lthy
+    |>> (fn {prefix, result, ...} => (prefix, result))
   handle OLD_PRIMREC () =>
     Old_Primrec.primrec_simple int fixes ts lthy
-    |>> apsnd (fn (ts, thms) => (ts, [], ([], [thms]))) o apfst single
-    |>> apfst (map_split (rpair I));
+    |>> (fn {prefix, result = (ts, thms), ...} =>
+          (map_split (rpair I) [prefix], (ts, [], ([], [thms]))))
 
 fun gen_primrec old_primrec prep_spec int opts raw_fixes raw_specs lthy =
   let
@@ -648,8 +653,8 @@
   in
     lthy
     |> primrec_simple0 int plugins nonexhaustive transfer fixes (map snd specs)
-    |-> (fn ((names, qualifys), (ts, defs, (jss, simpss))) =>
-      Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
+    |-> (fn {prefix = (names, qualifys), types, result = (ts, defs, (jss, simpss))} =>
+      Spec_Rules.add (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))
@@ -657,7 +662,7 @@
   end
   handle OLD_PRIMREC () =>
     old_primrec int raw_fixes raw_specs lthy
-    |>> (fn (ts, thms) => (ts, [], [thms]));
+    |>> (fn {result = (ts, thms), ...} => (ts, [], [thms]));
 
 val primrec = gen_primrec Old_Primrec.primrec Specification.check_multi_specs;
 val primrec_cmd = gen_primrec Old_Primrec.primrec_cmd Specification.read_multi_specs;
diff -r 6b097aeb3650 -r bd3c10813cc4 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 26 22:13:36 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 6b097aeb3650 -r bd3c10813cc4 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Mar 26 22:13:36 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 (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 (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 6b097aeb3650 -r bd3c10813cc4 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/HOL/Tools/Function/function.ML	Tue Mar 26 22:13:36 2019 +0100
@@ -210,7 +210,7 @@
              lthy
              |> Local_Theory.declaration {syntax = false, pervasive = false}
                (fn phi => add_function_data (transform_function_data phi info'))
-             |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
+             |> Spec_Rules.add Spec_Rules.equational_recdef (fs, tsimps))
           end)
       end
   in
diff -r 6b097aeb3650 -r bd3c10813cc4 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Mar 26 22:13:36 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 ([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 6b097aeb3650 -r bd3c10813cc4 src/HOL/Tools/Nunchaku/nunchaku_collect.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Tue Mar 26 22:13:36 2019 +0100
@@ -506,7 +506,7 @@
           if card = Inf orelse card = Fin_or_Inf then
             spec_rules ()
           else
-            [(Spec_Rules.Equational, ([Logic.varify_global \<^term>\<open>finite\<close>],
+            [(Spec_Rules.equational, ([Logic.varify_global \<^term>\<open>finite\<close>],
                [Skip_Proof.make_thm thy (Logic.varify_global \<^prop>\<open>finite A = True\<close>)]))]
         end
       else
diff -r 6b097aeb3650 -r bd3c10813cc4 src/HOL/Tools/Old_Datatype/old_primrec.ML
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Tue Mar 26 22:13:36 2019 +0100
@@ -9,16 +9,18 @@
 signature OLD_PRIMREC =
 sig
   val primrec: bool -> (binding * typ option * mixfix) list ->
-    Specification.multi_specs -> local_theory -> (term list * thm list) * local_theory
+    Specification.multi_specs -> local_theory ->
+    {types: string list, result: term list * thm list} * local_theory
   val primrec_cmd: bool -> (binding * string option * mixfix) list ->
-    Specification.multi_specs_cmd -> local_theory -> (term list * thm list) * local_theory
+    Specification.multi_specs_cmd -> local_theory ->
+    {types: string list, result: term list * thm list} * local_theory
   val primrec_global: bool -> (binding * typ option * mixfix) list ->
     Specification.multi_specs -> theory -> (term list * thm list) * theory
   val primrec_overloaded: bool -> (string * (string * typ) * bool) list ->
     (binding * typ option * mixfix) list ->
     Specification.multi_specs -> theory -> (term list * thm list) * theory
-  val primrec_simple: bool -> ((binding * typ) * mixfix) list -> term list ->
-    local_theory -> (string * (term list * thm list)) * local_theory
+  val primrec_simple: bool -> ((binding * typ) * mixfix) list -> term list -> local_theory ->
+    {prefix: string, types: string list, result: term list * thm list} * local_theory
 end;
 
 structure Old_Primrec : OLD_PRIMREC =
@@ -195,13 +197,13 @@
 
 fun make_def ctxt fixes fs (fname, ls, rec_name) =
   let
-    val SOME (var, varT) = get_first (fn ((b, T), mx) =>
+    val SOME (var, varT) = get_first (fn ((b, T), mx: mixfix) =>
       if Binding.name_of b = fname then SOME ((b, mx), T) else NONE) fixes;
     val def_name = Thm.def_name (Long_Name.base_name fname);
     val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT])
       (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
     val rhs = singleton (Syntax.check_terms ctxt) (Type.constraint varT raw_rhs);
-  in (var, ((Binding.concealed (Binding.name def_name), []), rhs)) end;
+  in (var, ((Binding.concealed (Binding.name def_name), []): Attrib.binding, rhs)) end;
 
 
 (* find datatypes which contain all datatypes in tnames' *)
@@ -250,7 +252,7 @@
           (fn {context = ctxt', ...} =>
             EVERY [rewrite_goals_tac ctxt' rewrites, resolve_tac ctxt' [refl] 1])) eqs
       end;
-  in ((prefix, (fs, defs)), prove) end
+  in ((prefix, tnames, (fs, defs)), prove) end
   handle PrimrecError (msg, some_eqn) =>
     error ("Primrec definition error:\n" ^ msg ^
       (case some_eqn of
@@ -262,12 +264,13 @@
 
 fun primrec_simple int fixes ts lthy =
   let
-    val ((prefix, (_, defs)), prove) = distill lthy fixes ts;
+    val ((prefix, tnames, (_, defs)), prove) = distill lthy fixes ts;
   in
     lthy
     |> fold_map Local_Theory.define defs
     |> tap (uncurry (BNF_FP_Rec_Sugar_Util.print_def_consts int))
-    |-> (fn defs => `(fn lthy => (prefix, (map fst defs, prove lthy defs))))
+    |-> (fn defs =>
+      `(fn lthy => {prefix = prefix, types = tnames, result = (map fst defs, prove lthy defs)}))
   end;
 
 local
@@ -282,13 +285,13 @@
   in
     lthy
     |> primrec_simple int fixes (map snd spec)
-    |-> (fn (prefix, (ts, simps)) =>
-      Spec_Rules.add Spec_Rules.Equational (ts, simps)
+    |-> (fn {prefix, types, result = (ts, simps)} =>
+      Spec_Rules.add (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'') => 
-        Code.declare_default_eqns (map (rpair true) simps'')
-        #> pair (ts, simps''))))
+        #-> (fn (_, simps'') => 
+          Code.declare_default_eqns (map (rpair true) simps'')
+          #> pair {types = types, result = (ts, simps'')})))
   end;
 
 in
@@ -301,14 +304,14 @@
 fun primrec_global int fixes specs thy =
   let
     val lthy = Named_Target.theory_init thy;
-    val ((ts, simps), lthy') = primrec int fixes specs lthy;
+    val ({result = (ts, simps), ...}, lthy') = primrec int fixes specs lthy;
     val simps' = Proof_Context.export lthy' lthy simps;
   in ((ts, simps'), Local_Theory.exit_global lthy') end;
 
 fun primrec_overloaded int ops fixes specs thy =
   let
     val lthy = Overloading.overloading ops thy;
-    val ((ts, simps), lthy') = primrec int fixes specs lthy;
+    val ({result = (ts, simps), ...}, lthy') = primrec int fixes specs lthy;
     val simps' = Proof_Context.export lthy' lthy simps;
   in ((ts, simps'), Local_Theory.exit_global lthy') end;
 
diff -r 6b097aeb3650 -r bd3c10813cc4 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/HOL/Tools/record.ML	Tue Mar 26 22:13:36 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])
+    Spec_Rules.add_global Spec_Rules.equational ([head], [rule])
   end;
 
 (* definition *)
diff -r 6b097aeb3650 -r bd3c10813cc4 src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/Pure/Isar/spec_rules.ML	Tue Mar 26 22:13:36 2019 +0100
@@ -8,8 +8,13 @@
 
 signature SPEC_RULES =
 sig
-  datatype rough_classification = Equational | Inductive | Co_Inductive | Unknown
+  datatype recursion = Primrec of string list | Recdef | Unknown_Recursion
+  val recursion_ord: recursion * recursion -> order
+  datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown
   val rough_classification_ord: rough_classification * rough_classification -> order
+  val equational_primrec: string list -> rough_classification
+  val equational_recdef: rough_classification
+  val equational: rough_classification
   val is_equational: rough_classification -> bool
   val is_inductive: rough_classification -> bool
   val is_co_inductive: rough_classification -> bool
@@ -26,14 +31,28 @@
 structure Spec_Rules: SPEC_RULES =
 struct
 
+(* recursion *)
+
+datatype recursion = Primrec of string list | Recdef | Unknown_Recursion;
+
+fun recursion_ord (Primrec Ts1, Primrec Ts2) = list_ord fast_string_ord (Ts1, Ts2)
+  | recursion_ord rs =
+      int_ord (apply2 (fn Primrec _ => 0 | Recdef => 1 | Unknown_Recursion => 2) rs);
+
+
 (* rough classification *)
 
-datatype rough_classification = Equational | Inductive | Co_Inductive | Unknown;
+datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown;
+
+fun rough_classification_ord (Equational r1, Equational r2) = recursion_ord (r1, r2)
+  | rough_classification_ord cs =
+      int_ord (apply2 (fn Equational _ => 0 | Inductive => 1 | Co_Inductive => 2 | Unknown => 3) cs);
 
-val rough_classification_ord =
-  int_ord o apply2 (fn Equational => 0 | Inductive => 1 | Co_Inductive => 2 | Unknown => 3);
+val equational_primrec = Equational o Primrec;
+val equational_recdef = Equational Recdef;
+val equational = Equational Unknown_Recursion;
 
-val is_equational = fn Equational => true | _ => false;
+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_unknown = fn Unknown => true | _ => false;
@@ -48,8 +67,8 @@
   type T = spec Item_Net.T;
   val empty : T =
     Item_Net.init
-      (fn ((class1, (ts1, ths1)), (class2, (ts2, ths2))) =>
-        rough_classification_ord (class1, class2) = EQUAL andalso
+      (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);
diff -r 6b097aeb3650 -r bd3c10813cc4 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Mar 26 22:13:36 2019 +0100
@@ -263,7 +263,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 Spec_Rules.Equational ([lhs], [th]);
+    val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.equational ([lhs], [th]);
 
     val ([(def_name, [th'])], lthy4) = lthy3
       |> Local_Theory.notes [((name, atts), [([th], [])])];
diff -r 6b097aeb3650 -r bd3c10813cc4 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/Pure/Proof/extraction.ML	Tue Mar 26 22:13:36 2019 +0100
@@ -801,7 +801,7 @@
            [((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 Spec_Rules.equational ([head], [def_thm])
            #> Code.declare_default_eqns_global [(def_thm, true)])
       end;
 
diff -r 6b097aeb3650 -r bd3c10813cc4 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Tue Mar 26 22:13:36 2019 +0100
@@ -101,6 +101,14 @@
   (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
 
 
+(* spec rules *)
+
+fun primrec_types ctxt const =
+  Spec_Rules.retrieve ctxt (Const const)
+  |> get_first (fn (Spec_Rules.Equational (Spec_Rules.Primrec types), _) => SOME types | _ => NONE)
+  |> the_default [];
+
+
 (* locales content *)
 
 fun locale_content thy loc =
@@ -230,17 +238,21 @@
     (* consts *)
 
     val encode_const =
-      let open XML.Encode Term_XML.Encode
-      in pair encode_syntax (pair (list string) (pair typ (pair (option term) bool))) end;
+      let open XML.Encode Term_XML.Encode in
+        pair encode_syntax
+          (pair (list string) (pair typ (pair (option term) (pair bool (list string)))))
+      end;
 
     fun export_const c (T, abbrev) =
       let
         val syntax = get_syntax_const thy_ctxt c;
-        val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
+        val U = Logic.unvarifyT_global T;
+        val U0 = Type.strip_sorts U;
+        val primrec_types = primrec_types thy_ctxt (c, U);
         val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts);
-        val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
-        val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type T');
-      in encode_const (syntax, (args, (T', (abbrev', propositional)))) end;
+        val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, U0));
+        val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
+      in encode_const (syntax, (args, (U0, (abbrev', (propositional, primrec_types))))) end;
 
     val _ =
       export_entities "consts" (SOME oo export_const) Sign.const_space
diff -r 6b097aeb3650 -r bd3c10813cc4 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Tue Mar 26 14:23:18 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala	Tue Mar 26 22:13:36 2019 +0100
@@ -252,7 +252,8 @@
     typargs: List[String],
     typ: Term.Typ,
     abbrev: Option[Term.Term],
-    propositional: Boolean)
+    propositional: Boolean,
+    primrec_types: List[String])
   {
     def cache(cache: Term.Cache): Const =
       Const(entity.cache(cache),
@@ -260,20 +261,23 @@
         typargs.map(cache.string(_)),
         cache.typ(typ),
         abbrev.map(cache.term(_)),
-        propositional)
+        propositional,
+        primrec_types.map(cache.string(_)))
   }
 
   def read_consts(provider: Export.Provider): List[Const] =
     provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.CONST, tree)
-        val (syntax, (args, (typ, (abbrev, propositional)))) =
+        val (syntax, (args, (typ, (abbrev, (propositional, primrec_types))))) =
         {
           import XML.Decode._
-          pair(decode_syntax, pair(list(string),
-            pair(Term_XML.Decode.typ, pair(option(Term_XML.Decode.term), bool))))(body)
+          pair(decode_syntax,
+            pair(list(string),
+              pair(Term_XML.Decode.typ,
+                pair(option(Term_XML.Decode.term), pair(bool, list(string))))))(body)
         }
-        Const(entity, syntax, args, typ, abbrev, propositional)
+        Const(entity, syntax, args, typ, abbrev, propositional, primrec_types)
       })