# HG changeset patch
# User blanchet
# Date 1392360825 -3600
# Node ID 78a06c7b5b87d34222d4b01860e658e8601f8d16
# Parent  ce676a750575ef446b5280f8831fab3157291805
added 'Spec_Rules' for 'primcorec'

diff -r ce676a750575 -r 78a06c7b5b87 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Feb 13 22:35:38 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Feb 14 07:53:45 2014 +0100
@@ -1034,9 +1034,9 @@
 
     val goalss = nchotomy_goalss @ exclude_goalss;
 
-    fun prove thmss'' def_thms' lthy =
+    fun prove thmss'' def_infos lthy =
       let
-        val def_thms = map (snd o snd) def_thms';
+        val def_thms = map (snd o snd) def_infos;
 
         val (nchotomy_thmss, exclude_thmss) =
           (map2 append (take actual_nn thmss'') nchotomy_taut_thmss, drop actual_nn thmss'');
@@ -1332,7 +1332,12 @@
           |> map (fn (thmN, thms, attrs) =>
             ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
       in
-        lthy |> Local_Theory.notes (notes @ common_notes) |> snd
+        lthy
+        |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat sel_thmss)
+        |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat ctr_thmss)
+        |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat code_thmss)
+        |> Local_Theory.notes (notes @ common_notes)
+        |> snd
       end;
 
     fun after_qed thmss' = fold_map Local_Theory.define defs #-> prove thmss';