src/HOL/Codegenerator_Test/Generate_Target_String_Literals.thy

--- a/src/HOL/Codegenerator_Test/Generate_Target_String_Literals.thy	Tue Jan 28 07:17:30 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Target_String_Literals.thy	Tue Jan 28 13:02:42 2025 +0100
@@ -7,7 +7,10 @@
   "HOL-Library.Code_Test"
 begin
 
-definition computations where
+context
+begin
+
+qualified definition computations where
   \<open>computations = (
     STR ''abc'' + STR 0x20 + STR ''def'',
     String.implode ''abc'',
@@ -18,7 +21,7 @@
     STR ''abc'' < STR ''def''
   )\<close>
 
-definition results where
+qualified definition results where
   \<open>results = (
     STR ''abc def'',
     STR ''abc'',
@@ -29,7 +32,7 @@
     True
   )\<close>
 
-definition check where
+qualified definition check where
   \<open>check \<longleftrightarrow> computations = results\<close>
 
 lemma check
@@ -41,8 +44,8 @@
 lemma check
   by eval
 
-test_code check in OCaml
-test_code check in GHC
 test_code check in Scala
 
 end
+
+end