Updates for Isabelle2025

Author: simondfoster

Z_Machine.ML

@@ -253,8 +253,8 @@ fun chantype_name n = n ^ "_chan"
 fun zmachine_sem (ZMachine {name = n, state = s, init = i, inv = inv, operations = ops, ends = e}) thy =
   let open Syntax; open HOLogic; open Lift_Expr
     val ctx = Named_Target.theory_init thy
-    val cs = map (fn n => (firstLower n, YXML.content_of (string_of_typ ctx (get_zop_ptype n ctx)))) ops @
-             map (fn n => (firstLower n ^ "_Out", YXML.content_of (string_of_typ ctx (get_zop_outtype n ctx)))) ops
+    val cs = map (fn n => (firstLower n, XML.content_of (YXML.parse_body (string_of_typ ctx (get_zop_ptype n ctx))))) ops @
+             map (fn n => (firstLower n ^ "_Out", XML.content_of (YXML.parse_body (string_of_typ ctx (get_zop_outtype n ctx))))) ops
     val st = read_typ ctx s
     val inve = mk_lift_expr ctx (parse_term ctx inv)
     val init = parse_term ctx i

Z_Machine.thy

@@ -6,7 +6,7 @@ theory Z_Machine
     and "over" "init" "invariant" "operations" "until" "params" "output" "pre" "update" "\<in>" "promote" "emit" "extends"
 begin
 
-expr_vars
+declare [[literal_variables=false]]
 
 named_theorems z_machine_defs
 
@@ -120,7 +120,9 @@ text \<open> Function to show the channel of an operation \<close>
 
 definition show_op_channel :: "String.literal \<Rightarrow> 'a::show \<Rightarrow> String.literal" where
 "show_op_channel c p = c + STR '' '' + show p"
-                
+
+ML \<open>open YXML\<close>
+
 ML_file \<open>Z_Machine.ML\<close>
 
 ML \<open>
@@ -139,7 +141,7 @@ code_datatype pfun_of_alist pfun_of_map pfun_entries
 
 setup \<open> Explorer_Lib.switch_to_quotes \<close>
 
-lit_vars
+declare [[literal_variables]]
 
 text \<open> Change the default target of string syntax to be literals. Literals are much better for
   code generation, and also provide more control since they are a distinct type to lists.
@@ -150,10 +152,10 @@ bundle literal_syntax
 begin
 
 no_syntax
-  "_String" :: "str_position \<Rightarrow> string"    ("_")
+  "_String" :: "str_position \<Rightarrow> string" (\<open>(\<open>open_block notation=\<open>literal string\<close>\<close>_)\<close>)
 
 syntax
-  "_Literal" :: "str_position \<Rightarrow> String.literal"   ("_")
+  "_Literal" :: "str_position \<Rightarrow> String.literal"  (\<open>(\<open>open_block notation=\<open>literal string\<close>\<close>_)\<close>)
 
 end
 
@@ -226,6 +228,6 @@ code_printing
 | constant "show_set_inst.show_set" \<rightharpoonup> (Haskell) "Prelude.show"
 | class_instance "set" :: "show" \<rightharpoonup> (Haskell) -
 
-code_reserved Haskell List_Set
+code_reserved (Haskell) List_Set
 
 end