don't declare ctr view primcorec theorems as simp (they loop)
authortraytel
Thu, 19 Sep 2013 17:38:03 +0200
changeset 53736 82799e03fff7
parent 53735 99331dac1e1c
child 53737 eab25a77af39
don't declare ctr view primcorec theorems as simp (they loop)
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))