# HG changeset patch
# User haftmann
# Date 1534505194 0
# Node ID 1db9fef36f128fe199551bf0c92469fcdf5f8b61
# Parent  23a5e7fba8377ecf440361a2f228d9c8ddaeab35
tuned

diff -r 23a5e7fba837 -r 1db9fef36f12 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Fri Aug 17 11:26:31 2018 +0000
+++ b/src/Pure/Isar/code.ML	Fri Aug 17 11:26:34 2018 +0000
@@ -1521,25 +1521,30 @@
 fun code_attribute f = Thm.declaration_attribute
   (fn thm => Context.mapping (f thm) I);
 
-fun code_const_attribute f cs =
-  code_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs));
+fun code_thm_attribute g f =
+  g |-- Scan.succeed (code_attribute f);
+
+fun code_const_attribute g f =
+  g -- Args.colon |-- Scan.repeat1 Parse.term
+    >> (fn ts => code_attribute (K (fold (fn t => fn thy => f (read_const thy t) thy) ts)));
 
 val _ = Theory.setup
   (let
     val code_attribute_parser =
-      Args.$$$ "equation" |-- Scan.succeed (code_attribute
-          (fn thm => generic_add_eqn Liberal (thm, true)))
-      || Args.$$$ "nbe" |-- Scan.succeed (code_attribute
-          (fn thm => generic_add_eqn Liberal (thm, false)))
-      || Args.$$$ "abstract" |-- Scan.succeed (code_attribute
-          (generic_declare_abstract_eqn Liberal))
-      || Args.$$$ "abstype" |-- Scan.succeed (code_attribute
-          (generic_declare_abstype Liberal))
-      || Args.del |-- Scan.succeed (code_attribute del_eqn_global)
-      || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term
-          >> code_const_attribute declare_aborting_global)
-      || Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term
-          >> code_const_attribute declare_unimplemented_global)
+      code_thm_attribute (Args.$$$ "equation")
+        (fn thm => generic_add_eqn Liberal (thm, true))
+      || code_thm_attribute (Args.$$$ "nbe")
+          (fn thm => generic_add_eqn Liberal (thm, false))
+      || code_thm_attribute (Args.$$$ "abstract")
+          (generic_declare_abstract_eqn Liberal)
+      || code_thm_attribute (Args.$$$ "abstype")
+          (generic_declare_abstype Liberal)
+      || code_thm_attribute Args.del
+          del_eqn_global
+      || code_const_attribute (Args.$$$ "abort")
+          declare_aborting_global
+      || code_const_attribute (Args.$$$ "drop")
+          declare_unimplemented_global
       || Scan.succeed (code_attribute
           add_maybe_abs_eqn_liberal);
   in