proper local context

--- a/src/HOL/Library/RBT_Set.thy	Sun Jul 11 21:29:54 2021 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Mon Jul 12 11:41:02 2021 +0000
@@ -709,6 +709,48 @@
 context
 begin
 
+declare [[code drop: Gcd_fin Lcm_fin \<open>Gcd :: _ \<Rightarrow> nat\<close> \<open>Gcd :: _ \<Rightarrow> int\<close> \<open>Lcm :: _ \<Rightarrow> nat\<close> \<open>Lcm :: _ \<Rightarrow> int\<close>]]
+
+lemma [code]:
+  "Gcd\<^sub>f\<^sub>i\<^sub>n (Set t) = fold_keys gcd t (0::'a::{semiring_gcd, linorder})"
+proof -
+  have "comp_fun_commute (gcd :: 'a \<Rightarrow> _)"
+    by standard (simp add: fun_eq_iff ac_simps)
+  with finite_fold_fold_keys [of _ 0 t]
+  have "Finite_Set.fold gcd 0 (Set t) = fold_keys gcd t 0"
+    by blast
+  then show ?thesis
+    by (simp add: Gcd_fin.eq_fold)
+qed
+    
+lemma [code]:
+  "Gcd (Set t) = (Gcd\<^sub>f\<^sub>i\<^sub>n (Set t) :: nat)"
+  by simp
+
+lemma [code]:
+  "Gcd (Set t) = (Gcd\<^sub>f\<^sub>i\<^sub>n (Set t) :: int)"
+  by simp
+
+lemma [code]:
+  "Lcm\<^sub>f\<^sub>i\<^sub>n (Set t) = fold_keys lcm t (1::'a::{semiring_gcd, linorder})"
+proof -
+  have "comp_fun_commute (lcm :: 'a \<Rightarrow> _)"
+    by standard (simp add: fun_eq_iff ac_simps)
+  with finite_fold_fold_keys [of _ 1 t]
+  have "Finite_Set.fold lcm 1 (Set t) = fold_keys lcm t 1"
+    by blast
+  then show ?thesis
+    by (simp add: Lcm_fin.eq_fold)
+qed
+
+lemma [code drop: "Lcm :: _ \<Rightarrow> nat", code]:
+  "Lcm (Set t) = (Lcm\<^sub>f\<^sub>i\<^sub>n (Set t) :: nat)"
+  by simp
+
+lemma [code drop: "Lcm :: _ \<Rightarrow> int", code]:
+  "Lcm (Set t) = (Lcm\<^sub>f\<^sub>i\<^sub>n (Set t) :: int)"
+  by simp
+
 qualified definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a"
   where [code_abbrev]: "Inf' = Inf"
 
@@ -723,49 +765,6 @@
   "Sup' (Set t) = (if RBT.is_empty t then bot else r_max_opt t)"
   by (simp add: Sup'_def Sup_Set_fold)
 
-lemma [code drop: Gcd_fin, code]:
-  "Gcd\<^sub>f\<^sub>i\<^sub>n (Set t) = fold_keys gcd t (0::'a::{semiring_gcd, linorder})"
-proof -
-  have "comp_fun_commute (gcd :: 'a \<Rightarrow> _)"
-    by standard (simp add: fun_eq_iff ac_simps)
-  with finite_fold_fold_keys [of _ 0 t]
-  have "Finite_Set.fold gcd 0 (Set t) = fold_keys gcd t 0"
-    by blast
-  then show ?thesis
-    by (simp add: Gcd_fin.eq_fold)
-qed
-    
-lemma [code drop: "Gcd :: _ \<Rightarrow> nat", code]:
-  "Gcd (Set t) = (Gcd\<^sub>f\<^sub>i\<^sub>n (Set t) :: nat)"
-  by simp
-
-lemma [code drop: "Gcd :: _ \<Rightarrow> int", code]:
-  "Gcd (Set t) = (Gcd\<^sub>f\<^sub>i\<^sub>n (Set t) :: int)"
-  by simp
-
-lemma [code drop: Lcm_fin,code]:
-  "Lcm\<^sub>f\<^sub>i\<^sub>n (Set t) = fold_keys lcm t (1::'a::{semiring_gcd, linorder})"
-proof -
-  have "comp_fun_commute (lcm :: 'a \<Rightarrow> _)"
-    by standard (simp add: fun_eq_iff ac_simps)
-  with finite_fold_fold_keys [of _ 1 t]
-  have "Finite_Set.fold lcm 1 (Set t) = fold_keys lcm t 1"
-    by blast
-  then show ?thesis
-    by (simp add: Lcm_fin.eq_fold)
-qed
-
-qualified definition Lcm' :: "'a :: semiring_Gcd set \<Rightarrow> 'a"
-  where [code_abbrev]: "Lcm' = Lcm"
-
-lemma [code drop: "Lcm :: _ \<Rightarrow> nat", code]:
-  "Lcm (Set t) = (Lcm\<^sub>f\<^sub>i\<^sub>n (Set t) :: nat)"
-  by simp
-
-lemma [code drop: "Lcm :: _ \<Rightarrow> int", code]:
-  "Lcm (Set t) = (Lcm\<^sub>f\<^sub>i\<^sub>n (Set t) :: int)"
-  by simp
-
 end
 
 lemma sorted_list_set[code]: "sorted_list_of_set (Set t) = RBT.keys t"

--- 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);