lib: Isabelle2023 update

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lib/Lib.thy

@@ -2237,7 +2237,7 @@ lemma map_of_zip_is_index:
 
 lemma map_of_zip_take_update:
   "\<lbrakk>i < length xs; length xs \<le> length ys; distinct xs\<rbrakk>
-  \<Longrightarrow> map_of (zip (take i xs) ys)(xs ! i \<mapsto> (ys ! i)) = map_of (zip (take (Suc i) xs) ys)"
+  \<Longrightarrow> (map_of (zip (take i xs) ys)) (xs ! i \<mapsto> ys ! i) = map_of (zip (take (Suc i) xs) ys)"
   apply (rule ext, rename_tac x)
   apply (case_tac "x=xs ! i"; clarsimp)
    apply (rule map_of_is_SomeI[symmetric])

lib/ML_Goal.thy

@@ -109,7 +109,7 @@ fun begin_proof ((name, attrs): Attrib.binding, ml_block: Input.source) ctxt =
             val ((res_name, res), ctxt') =
                 Local_Theory.note (binding, thms) ctxt;
             val _ =
-                Proof_Display.print_results true start_pos ctxt'
+                Proof_Display.print_results { interactive = true, pos = start_pos, proof_state = true } ctxt'
                   (("theorem", res_name), [("", res)])
           in ctxt' end
     in

lib/Qualify.thy

@@ -110,7 +110,7 @@ val _ =
           Toplevel.theory (set_global_qualify {name = str, target_name = case target of SOME (nm, _) => nm | _ => str})));
 
 fun syntax_alias global_alias local_alias b name =
-  Local_Theory.declaration {syntax = true, pervasive = true} (fn phi =>
+  Local_Theory.declaration {syntax = true, pos = Position.none, pervasive = true} (fn phi =>
     let val b' = Morphism.binding phi b
     in Context.mapping (global_alias b' name) (local_alias b' name) end);
 

lib/Requalify.thy

@@ -49,7 +49,7 @@ in
 end
 
 fun syntax_alias global_alias local_alias b (name : string) =
-  Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
+  Local_Theory.declaration {syntax = false, pos = Position.none, pervasive = true} (fn phi =>
     let val b' = Morphism.binding phi b
     in Context.mapping (global_alias b' name) (local_alias b' name) end);
 

lib/defs.ML

@@ -29,7 +29,7 @@ val opt_unchecked_overloaded =
       @{keyword "overloaded"} >> K (false, true)) --| @{keyword ")"})) (false, false);
 
 fun syntax_alias global_alias local_alias b name =
-  Local_Theory.declaration {syntax = true, pervasive = true} (fn phi =>
+  Local_Theory.declaration {syntax = true, pos = Position.none, pervasive = true} (fn phi =>
     let val b' = Morphism.binding phi b
     in Context.mapping (global_alias b' name) (local_alias b' name) end);