Updated Z_Machines to use the new type signature for generating chann…

…els types

Z_Machine.ML

@@ -250,17 +250,18 @@ fun zmachine_body_sem n st init inve ops ends ctx =
 
 fun chantype_name n = n ^ "_chan"
 
-fun zmachine_sem (ZMachine {name = n, state = s, init = i, inv = inv, operations = ops, ends = e}) ctx =
+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 st = read_typ ctx s
     val inve = mk_lift_expr ctx (parse_term ctx inv)
     val init = parse_term ctx i
     val ends = mk_lift_expr ctx (parse_term ctx e)
-  in Channel_Type.compile_chantype (chantype_name n, cs) ctx |>
-     Named_Target.theory_init o mk_chan_show_inst (chantype_name n) ops o Local_Theory.exit_global |>
-     zmachine_body_sem n st init inve ops ends
+  in Channel_Type.compile_chantype (chantype_name n, cs) thy |>
+     Named_Target.theory_init o mk_chan_show_inst (chantype_name n) ops |>
+     Local_Theory.exit_global o zmachine_body_sem n st init inve ops ends
   end
 
 val parse_param = 

Z_Machine.thy

@@ -125,7 +125,7 @@ ML_file \<open>Z_Machine.ML\<close>
 
 ML \<open>
 Outer_Syntax.command @{command_keyword zmachine} "define a Z machine"
-    (Z_Machine.parse_zmachine >> (Toplevel.local_theory NONE NONE o Z_Machine.zmachine_sem));
+    (Z_Machine.parse_zmachine >> (Toplevel.theory o Z_Machine.zmachine_sem));
 
 Outer_Syntax.command @{command_keyword zoperation} "define a Z operation"
     (Z_Machine.parse_operation >> (Toplevel.local_theory NONE NONE o Z_Machine.mk_zop));