src/HOL/Tools/recdef.ML

                congs wfs name R eqs;
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
     val simp_att =
       if null tcs then [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]
       else [];
-
+    fun specs_of simps =
+      let
+        fun dest_eqn th = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))
+        val ts = distinct (op =) (map dest_eqn simps)
+      in (ts, simps) end
     val ((simps' :: rules', [induct']), thy) =
       thy
       |> Sign.add_path bname
       |> PureThy.add_thmss
         (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
-      ||>> PureThy.add_thms [((Binding.name "induct", induct), [])];
+      ||>> PureThy.add_thms [((Binding.name "induct", induct), [])]
+      ||> Spec_Rules.add_global Spec_Rules.Equational (specs_of (flat rules));
     val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
     val thy =
       thy
       |> put_recdef name result
       |> Sign.parent_path;