--- a/src/Pure/Isar/code.ML Sun Jul 11 21:29:54 2021 +0200
+++ b/src/Pure/Isar/code.ML Mon Jul 12 11:41:02 2021 +0000
@@ -1528,11 +1528,11 @@
(fn thm => Context.mapping (f thm) I);
fun code_thm_attribute g f =
- g |-- Scan.succeed (code_attribute f);
+ Scan.lift (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)));
+ Scan.lift (g -- Args.colon) |-- Scan.repeat1 Args.term
+ >> (fn ts => code_attribute (K (fold (fn t => fn thy => f ((check_const thy o Logic.unvarify_types_global) t) thy) ts)));
val _ = Theory.setup
(let
@@ -1554,7 +1554,7 @@
|| Scan.succeed (code_attribute
add_maybe_abs_eqn_liberal);
in
- Attrib.setup \<^binding>\<open>code\<close> (Scan.lift code_attribute_parser)
+ Attrib.setup \<^binding>\<open>code\<close> code_attribute_parser
"declare theorems for code generation"
end);