# HG changeset patch
# User blanchet
# Date 1455638500 -3600
# Node ID 8c3eec5812d835dc4d3642e13d82d04cdbb12d38
# Parent  d2db9719ffb827313e043664001fbb68a3d17a25
avoid duplicate theorems in 'primrec's result when invoked programmatically

diff -r d2db9719ffb8 -r 8c3eec5812d8 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Feb 15 18:27:17 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Feb 16 17:01:40 2016 +0100
@@ -607,8 +607,9 @@
     lthy'
     |> fold_map Local_Theory.define defs
     |-> (fn defs => fn lthy =>
-      let val ((jss, simpss), lthy) = prove lthy defs;
-      in ((names, (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy) end)
+      let val ((jss, simpss), lthy) = prove lthy defs in
+        ((names, (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy)
+      end)
   end;
 
 fun primrec_simple fixes ts lthy =
@@ -649,7 +650,7 @@
     |-> (fn (names, (ts, defs, (jss, simpss))) =>
       Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
       #> Local_Theory.notes (mk_notes jss names simpss)
-      #>> (fn notes => (ts, defs, map snd notes)))
+      #>> (fn notes => (ts, defs, map_filter (fn ("", _) => NONE | (_, thms) => SOME thms) notes)))
   end
   handle OLD_PRIMREC () =>
     old_primrec raw_fixes raw_specs lthy