# HG changeset patch
# User traytel
# Date 1379605083 -7200
# Node ID 82799e03fff7f1fbacf495208abbfad546618a37
# Parent  99331dac1e1ceb35d68e3346dccefae996817f91
don't declare ctr view primcorec theorems as simp (they loop)

diff -r 99331dac1e1c -r 82799e03fff7 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 19 16:12:43 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 19 17:38:03 2013 +0200
@@ -839,7 +839,7 @@
           fun_names ~~ map5 (maps oooo prove_ctr) disc_thmss sel_thmss
             disc_eqnss sel_eqnss (map #ctr_specs corec_specs)
           |> map (fn (fun_name, thms) =>
-            ((Binding.qualify true fun_name (@{binding ctr}), simp_attrs), [(thms, [])]));
+            ((Binding.qualify true fun_name (@{binding ctr}), []), [(thms, [])]));
       in
         lthy |> snd o Local_Theory.notes
           (filter (not o null o fst o the_single o snd) (disc_notes @ sel_notes @ ctr_notes))