# HG changeset patch
# User wenzelm
# Date 1333299892 -7200
# Node ID afacccb4e2c7d0f2265ce08d8bda551aeec20cb4
# Parent  23654b331d5cefa7ceb191ff05e686b6994c1a39
simplified;

diff -r 23654b331d5c -r afacccb4e2c7 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Apr 01 18:01:19 2012 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Apr 01 19:04:52 2012 +0200
@@ -1420,14 +1420,12 @@
     val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
       (maps_modes result_thms)
     val qname = #qname (dest_steps steps)
-    (* FIXME !? *)
-    val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
-      (fn thm => Context.mapping (Code.add_eqn thm) I))))
+    val attrib = Thm.declaration_attribute (fn thm => Context.mapping (Code.add_eqn thm) I)
     val thy''' =
       cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...." (fn _ =>
       fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
       [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
-        [attrib thy ])] thy))
+        [attrib])] thy))
       result_thms' thy'' |> Theory.checkpoint)
   in
     thy'''