# HG changeset patch
# User paulson
# Date 1737154813 0
# Node ID e4ff4a4ee4ec277373255efa18f117afd424af7f
# Parent  a4c0f9d124403b1a0b51e2b4f6c7383a25c98900# Parent  1c003b308c98c35ba8b4b805b3a4972d2537988e
merged

diff -r 1c003b308c98 -r e4ff4a4ee4ec NEWS
--- a/NEWS	Fri Jan 17 20:24:09 2025 +0000
+++ b/NEWS	Fri Jan 17 23:00:13 2025 +0000
@@ -298,6 +298,9 @@
       image_mset_diff_if_inj
       minus_add_mset_if_not_in_lhs[simp]
 
+* Theory "HOL-Library.Suc_Notation" provides compact notation for nested
+Suc terms.
+
 * Transitional theory "HOL.Divides" moved to "HOL-Library.Divides" and
 supposed to be removed in a future release. Minor INCOMPATIBILITY.
 Import "HOL-Library.Divides" and keep an eye on qualified names with prefix
diff -r 1c003b308c98 -r e4ff4a4ee4ec etc/build.props
--- a/etc/build.props	Fri Jan 17 20:24:09 2025 +0000
+++ b/etc/build.props	Fri Jan 17 23:00:13 2025 +0000
@@ -27,6 +27,7 @@
   src/Pure/Admin/component_eptcs.scala \
   src/Pure/Admin/component_foiltex.scala \
   src/Pure/Admin/component_fonts.scala \
+  src/Pure/Admin/component_hol_light.scala \
   src/Pure/Admin/component_hugo.scala \
   src/Pure/Admin/component_javamail.scala \
   src/Pure/Admin/component_jcef.scala \
diff -r 1c003b308c98 -r e4ff4a4ee4ec etc/settings
--- a/etc/settings	Fri Jan 17 20:24:09 2025 +0000
+++ b/etc/settings	Fri Jan 17 23:00:13 2025 +0000
@@ -164,7 +164,7 @@
 
 ISABELLE_OPAM_ROOT="$USER_HOME/.opam"
 
-ISABELLE_OCAML_VERSION="ocaml-base-compiler.4.12.0"
+ISABELLE_OCAML_VERSION="ocaml-base-compiler.4.14.1"
 
 
 ###
diff -r 1c003b308c98 -r e4ff4a4ee4ec lib/Tools/ocaml_setup
--- a/lib/Tools/ocaml_setup	Fri Jan 17 20:24:09 2025 +0000
+++ b/lib/Tools/ocaml_setup	Fri Jan 17 23:00:13 2025 +0000
@@ -2,20 +2,6 @@
 #
 # Author: Makarius
 #
-# DESCRIPTION: setup OCaml via OPAM
-
-set -e
+# DESCRIPTION: setup OCaml for Isabelle via OPAM
 
-if [ -d "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin" ]
-then
-  isabelle_opam switch -y "$ISABELLE_OCAML_VERSION"
-elif [ -e "$ISABELLE_OPAM_ROOT/config" ]
-then
-  isabelle_opam switch create -y "$ISABELLE_OCAML_VERSION"
-else
-  mkdir -p "$ISABELLE_OPAM_ROOT"
-  cd "$ISABELLE_OPAM_ROOT"
-  isabelle_opam init -y --disable-sandboxing --no-setup --compiler="$ISABELLE_OCAML_VERSION"
-fi
-
-isabelle_opam install -y zarith
+isabelle ocaml_setup_base && isabelle_opam install -y zarith
diff -r 1c003b308c98 -r e4ff4a4ee4ec lib/Tools/ocaml_setup_base
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/ocaml_setup_base	Fri Jan 17 23:00:13 2025 +0000
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: setup OCaml base compiler via OPAM
+
+set -e
+
+if [ -d "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin" ]
+then
+  isabelle_opam switch -y "$ISABELLE_OCAML_VERSION"
+elif [ -e "$ISABELLE_OPAM_ROOT/config" ]
+then
+  isabelle_opam switch create -y "$ISABELLE_OCAML_VERSION"
+else
+  mkdir -p "$ISABELLE_OPAM_ROOT"
+  cd "$ISABELLE_OPAM_ROOT"
+  isabelle_opam init -y --disable-sandboxing --no-setup --compiler="$ISABELLE_OCAML_VERSION"
+fi
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/HOL/Import/Import_Setup.thy
--- a/src/HOL/Import/Import_Setup.thy	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/HOL/Import/Import_Setup.thy	Fri Jan 17 23:00:13 2025 +0000
@@ -3,7 +3,7 @@
     Author:     Alexander Krauss, QAware GmbH
 *)
 
-section \<open>Importer machinery and required theorems\<close>
+section \<open>Importer machinery\<close>
 
 theory Import_Setup
 imports Main
@@ -11,22 +11,6 @@
 begin
 
 ML_file \<open>import_data.ML\<close>
-
-lemma light_ex_imp_nonempty:
-  "P t \<Longrightarrow> \<exists>x. x \<in> Collect P"
-  by auto
-
-lemma typedef_hol2hollight:
-  assumes a: "type_definition Rep Abs (Collect P)"
-  shows "Abs (Rep a) = a \<and> P r = (Rep (Abs r) = r)"
-  by (metis type_definition.Rep_inverse type_definition.Abs_inverse
-      type_definition.Rep a mem_Collect_eq)
-
-lemma ext2:
-  "(\<And>x. f x = g x) \<Longrightarrow> f = g"
-  by auto
-
 ML_file \<open>import_rule.ML\<close>
 
 end
-
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/HOL/Import/import_data.ML
--- a/src/HOL/Import/import_data.ML	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/HOL/Import/import_data.ML	Fri Jan 17 23:00:13 2025 +0000
@@ -7,11 +7,10 @@
 
 signature IMPORT_DATA =
 sig
-  val get_const_map : string -> theory -> string option
-  val get_typ_map : string -> theory -> string option
-  val get_const_def : string -> theory -> thm option
-  val get_typ_def : string -> theory -> thm option
-
+  val get_const_map : theory -> string -> string option
+  val get_typ_map : theory -> string -> string option
+  val get_const_def : theory -> string -> thm option
+  val get_typ_def : theory -> string -> thm option
   val add_const_map : string -> string -> theory -> theory
   val add_const_map_cmd : string -> string -> theory -> theory
   val add_typ_map : string -> string -> theory -> theory
@@ -25,114 +24,110 @@
 
 structure Data = Theory_Data
 (
-  type T = {const_map: string Symtab.table, ty_map: string Symtab.table,
-            const_def: thm Symtab.table, ty_def: thm Symtab.table}
-  val empty = {const_map = Symtab.empty, ty_map = Symtab.empty,
-               const_def = Symtab.empty, ty_def = Symtab.empty}
+  type T =
+   {const_map: string Symtab.table, ty_map: string Symtab.table,
+    const_def: thm Symtab.table, ty_def: thm Symtab.table}
+  val empty =
+   {const_map = Symtab.empty, ty_map = Symtab.empty,
+    const_def = Symtab.empty, ty_def = Symtab.empty}
   fun merge
    ({const_map = cm1, ty_map = tm1, const_def = cd1, ty_def = td1},
     {const_map = cm2, ty_map = tm2, const_def = cd2, ty_def = td2}) : T =
     {const_map = Symtab.merge (K true) (cm1, cm2), ty_map = Symtab.merge (K true) (tm1, tm2),
-     const_def = Symtab.merge (K true) (cd1, cd2), ty_def = Symtab.merge (K true) (td1, td2)
-    }
+     const_def = Symtab.merge (K true) (cd1, cd2), ty_def = Symtab.merge (K true) (td1, td2)}
 )
 
-fun get_const_map s thy = Symtab.lookup (#const_map (Data.get thy)) s
-
-fun get_typ_map s thy = Symtab.lookup (#ty_map (Data.get thy)) s
-
-fun get_const_def s thy = Symtab.lookup (#const_def (Data.get thy)) s
+val get_const_map = Symtab.lookup o #const_map o Data.get
+val get_typ_map = Symtab.lookup o #ty_map o Data.get
+val get_const_def = Symtab.lookup o #const_def o Data.get
+val get_typ_def = Symtab.lookup o #ty_def o Data.get
 
-fun get_typ_def s thy = Symtab.lookup (#ty_def (Data.get thy)) s
-
-fun add_const_map s1 s2 thy =
+fun add_const_map c d =
   Data.map (fn {const_map, ty_map, const_def, ty_def} =>
-    {const_map = (Symtab.update (s1, s2) const_map), ty_map = ty_map,
-     const_def = const_def, ty_def = ty_def}) thy
+    {const_map = Symtab.update (c, d) const_map, ty_map = ty_map,
+     const_def = const_def, ty_def = ty_def})
 
-fun add_const_map_cmd s1 raw_s2 thy =
+fun add_const_map_cmd c s thy =
   let
     val ctxt = Proof_Context.init_global thy
-    val Const (s2, _) = Proof_Context.read_const {proper = true, strict = false} ctxt raw_s2
-  in add_const_map s1 s2 thy end
+    val d = dest_Const_name (Proof_Context.read_const {proper = true, strict = false} ctxt s)
+  in add_const_map c d thy end
 
-fun add_typ_map s1 s2 thy =
+fun add_typ_map c d =
   Data.map (fn {const_map, ty_map, const_def, ty_def} =>
-    {const_map = const_map, ty_map = (Symtab.update (s1, s2) ty_map),
-     const_def = const_def, ty_def = ty_def}) thy
+    {const_map = const_map, ty_map = (Symtab.update (c, d) ty_map),
+     const_def = const_def, ty_def = ty_def})
 
-fun add_typ_map_cmd s1 raw_s2 thy =
+fun add_typ_map_cmd c s thy =
   let
     val ctxt = Proof_Context.init_global thy
-    val Type (s2, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt raw_s2
-  in add_typ_map s1 s2 thy end
+    val d = dest_Type_name (Proof_Context.read_type_name {proper = true, strict = false} ctxt s)
+  in add_typ_map c d thy end
 
-fun add_const_def s th name_opt thy =
+fun add_const_def c th name_opt thy =
   let
-    val th = Thm.legacy_freezeT th
-    val name = case name_opt of
-         NONE => dest_Const_name (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th))))
-       | SOME n => n
-    val thy' = add_const_map s name thy
+    val th' = Thm.legacy_freezeT th
+    val d =
+      (case name_opt of
+        NONE => dest_Const_name (#1 (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))))
+      | SOME d => d)
   in
-    Data.map (fn {const_map, ty_map, const_def, ty_def} =>
+    thy
+    |> add_const_map c d
+    |> Data.map (fn {const_map, ty_map, const_def, ty_def} =>
       {const_map = const_map, ty_map = ty_map,
-       const_def = (Symtab.update (s, th) const_def), ty_def = ty_def}) thy'
+       const_def = (Symtab.update (c, th') const_def), ty_def = ty_def})
   end
 
-fun add_typ_def tyname absname repname th thy =
+fun add_typ_def type_name abs_name rep_name th thy =
   let
-    val th = Thm.legacy_freezeT th
-    val (l, _) = dest_comb (HOLogic.dest_Trueprop (Thm.prop_of th))
-    val (l, abst) = dest_comb l
-    val (_, rept) = dest_comb l
-    val absn = dest_Const_name abst
-    val repn = dest_Const_name rept
-    val nty = domain_type (fastype_of rept)
-    val ntyn = dest_Type_name nty
-    val thy2 = add_typ_map tyname ntyn thy
-    val thy3 = add_const_map absname absn thy2
-    val thy4 = add_const_map repname repn thy3
+    val th' = Thm.legacy_freezeT th
+    val \<^Const_>\<open>type_definition A _ for rep abs _\<close> = HOLogic.dest_Trueprop (Thm.prop_of th')
   in
-    Data.map (fn {const_map, ty_map, const_def, ty_def} =>
+    thy
+    |> add_typ_map type_name (dest_Type_name A)
+    |> add_const_map abs_name (dest_Const_name abs)
+    |> add_const_map rep_name (dest_Const_name rep)
+    |> Data.map (fn {const_map, ty_map, const_def, ty_def} =>
       {const_map = const_map, ty_map = ty_map,
-       const_def = const_def, ty_def = (Symtab.update (tyname, th) ty_def)}) thy4
+       const_def = const_def, ty_def = (Symtab.update (type_name, th') ty_def)})
   end
 
-val _ = Theory.setup
-  (Attrib.setup \<^binding>\<open>import_const\<close>
+val _ =
+  Theory.setup (Attrib.setup \<^binding>\<open>import_const\<close>
     (Scan.lift Parse.name --
       Scan.option (Scan.lift \<^keyword>\<open>:\<close> |-- Args.const {proper = true, strict = false}) >>
       (fn (s1, s2) => Thm.declaration_attribute
         (fn th => Context.mapping (add_const_def s1 th s2) I)))
-  "declare a theorem as an equality that maps the given constant")
+    "declare a theorem as an equality that maps the given constant")
 
-val _ = Theory.setup
-  (Attrib.setup \<^binding>\<open>import_type\<close>
+val _ =
+  Theory.setup (Attrib.setup \<^binding>\<open>import_type\<close>
     (Scan.lift (Parse.name -- Parse.name -- Parse.name) >>
       (fn ((tyname, absname), repname) => Thm.declaration_attribute
         (fn th => Context.mapping (add_typ_def tyname absname repname th) I)))
-  "declare a type_definition theorem as a map for an imported type with abs and rep")
+    "declare a type_definition theorem as a map for an imported type with abs and rep")
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>import_type_map\<close>
     "map external type name to existing Isabelle/HOL type name"
     ((Parse.name --| \<^keyword>\<open>:\<close>) -- Parse.type_const >>
-      (fn (ty_name1, ty_name2) => Toplevel.theory (add_typ_map_cmd ty_name1 ty_name2)))
+      (fn (c, d) => Toplevel.theory (add_typ_map_cmd c d)))
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>import_const_map\<close>
     "map external const name to existing Isabelle/HOL const name"
     ((Parse.name --| \<^keyword>\<open>:\<close>) -- Parse.const >>
-      (fn (cname1, cname2) => Toplevel.theory (add_const_map_cmd cname1 cname2)))
+      (fn (c, d) => Toplevel.theory (add_const_map_cmd c d)))
 
-(* Initial type and constant maps, for types and constants that are not
-   defined, which means their definitions do not appear in the proof dump *)
-val _ = Theory.setup
-  (add_typ_map "bool" \<^type_name>\<open>bool\<close> #>
-  add_typ_map "fun" \<^type_name>\<open>fun\<close> #>
-  add_typ_map "ind" \<^type_name>\<open>ind\<close> #>
-  add_const_map "=" \<^const_name>\<open>HOL.eq\<close> #>
-  add_const_map "@" \<^const_name>\<open>Eps\<close>)
+(*Initial type and constant maps, for types and constants that are not
+  defined, which means their definitions do not appear in the proof dump.*)
+val _ =
+  Theory.setup
+   (add_typ_map "bool" \<^type_name>\<open>bool\<close> #>
+    add_typ_map "fun" \<^type_name>\<open>fun\<close> #>
+    add_typ_map "ind" \<^type_name>\<open>ind\<close> #>
+    add_const_map "=" \<^const_name>\<open>HOL.eq\<close> #>
+    add_const_map "@" \<^const_name>\<open>Eps\<close>)
 
 end
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/HOL/Import/import_rule.ML	Fri Jan 17 23:00:13 2025 +0000
@@ -18,33 +18,25 @@
   val conj2 : thm -> thm
   val refl : cterm -> thm
   val abs : cterm -> thm -> thm
-  val mdef : string -> theory -> thm
+  val mdef : theory -> string -> thm
   val def : string -> cterm -> theory -> thm * theory
-  val mtydef : string -> theory -> thm
+  val mtydef : theory -> string -> thm
   val tydef :
     string -> string -> string -> cterm -> cterm -> thm -> theory -> thm * theory
-  val inst_type : (ctyp * ctyp) list -> thm -> theory -> thm
+  val inst_type : (ctyp * ctyp) list -> thm -> thm
   val inst : (cterm * cterm) list -> thm -> thm
-
-  type state
-  val init_state : state
-  val process_line : string -> (theory * state) -> (theory * state)
-  val process_file : Path.T -> theory -> theory
+  val import_file : Path.T -> theory -> theory
 end
 
 structure Import_Rule: IMPORT_RULE =
 struct
 
-val init_state = ((Inttab.empty, 0), (Inttab.empty, 0), (Inttab.empty, 0))
-
-type state = (ctyp Inttab.table * int) * (cterm Inttab.table * int) * (thm Inttab.table * int)
-
 fun implies_elim_all th = implies_elim_list th (map Thm.assume (cprems_of th))
 
 fun meta_mp th1 th2 =
   let
     val th1a = implies_elim_all th1
-    val th1b = Thm.implies_intr (strip_imp_concl (Thm.cprop_of th2)) th1a
+    val th1b = Thm.implies_intr (Thm.cconcl_of th2) th1a
     val th2a = implies_elim_all th2
     val th3 = Thm.implies_elim th1b th2a
   in
@@ -53,20 +45,19 @@
 
 fun meta_eq_to_obj_eq th =
   let
-    val (tml, tmr) = Thm.dest_binop (strip_imp_concl (Thm.cprop_of th))
-    val cty = Thm.ctyp_of_cterm tml
-    val i = Thm.instantiate' [SOME cty] [SOME tml, SOME tmr]
-      @{thm meta_eq_to_obj_eq}
+    val (t, u) = Thm.dest_equals (Thm.cconcl_of th)
+    val A = Thm.ctyp_of_cterm t
+    val rl = Thm.instantiate' [SOME A] [SOME t, SOME u] @{thm meta_eq_to_obj_eq}
   in
-    Thm.implies_elim i th
+    Thm.implies_elim rl th
   end
 
 fun beta ct = meta_eq_to_obj_eq (Thm.beta_conversion false ct)
 
 fun eq_mp th1 th2 =
   let
-    val (tm1l, tm1r) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th1)))
-    val i1 = Thm.instantiate' [] [SOME tm1l, SOME tm1r] @{thm iffD1}
+    val (Q, P) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th1))
+    val i1 = Thm.instantiate' [] [SOME Q, SOME P] @{thm iffD1}
     val i2 = meta_mp i1 th1
   in
     meta_mp i2 th2
@@ -74,13 +65,12 @@
 
 fun comb th1 th2 =
   let
-    val t1c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th1))
-    val t2c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th2))
-    val (cf, cg) = Thm.dest_binop t1c
-    val (cx, cy) = Thm.dest_binop t2c
-    val [fd, fr] = Thm.dest_ctyp (Thm.ctyp_of_cterm cf)
-    val i1 = Thm.instantiate' [SOME fd, SOME fr]
-      [SOME cf, SOME cg, SOME cx, SOME cy] @{thm cong}
+    val t1 = Thm.dest_arg (Thm.cconcl_of th1)
+    val t2 = Thm.dest_arg (Thm.cconcl_of th2)
+    val (f, g) = Thm.dest_binop t1
+    val (x, y) = Thm.dest_binop t2
+    val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm f)
+    val i1 = Thm.instantiate' [SOME A, SOME B] [SOME f, SOME g, SOME x, SOME y] @{thm cong}
     val i2 = meta_mp i1 th1
   in
     meta_mp i2 th2
@@ -88,10 +78,10 @@
 
 fun trans th1 th2 =
   let
-    val t1c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th1))
-    val t2c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th2))
-    val (r, s) = Thm.dest_binop t1c
-    val (_, t) = Thm.dest_binop t2c
+    val t1 = Thm.dest_arg (Thm.cconcl_of th1)
+    val t2 = Thm.dest_arg (Thm.cconcl_of th2)
+    val (r, s) = Thm.dest_binop t1
+    val t = Thm.dest_arg t2
     val ty = Thm.ctyp_of_cterm r
     val i1 = Thm.instantiate' [SOME ty] [SOME r, SOME s, SOME t] @{thm trans}
     val i2 = meta_mp i1 th1
@@ -101,14 +91,13 @@
 
 fun deduct th1 th2 =
   let
-    val th1c = strip_imp_concl (Thm.cprop_of th1)
-    val th2c = strip_imp_concl (Thm.cprop_of th2)
+    val th1c = Thm.cconcl_of th1
+    val th2c = Thm.cconcl_of th2
     val th1a = implies_elim_all th1
     val th2a = implies_elim_all th2
     val th1b = Thm.implies_intr th2c th1a
     val th2b = Thm.implies_intr th1c th2a
-    val i = Thm.instantiate' []
-      [SOME (Thm.dest_arg th1c), SOME (Thm.dest_arg th2c)] @{thm iffI}
+    val i = Thm.instantiate' [] [SOME (Thm.dest_arg th1c), SOME (Thm.dest_arg th2c)] @{thm iffI}
     val i1 = Thm.implies_elim i (Thm.assume (Thm.cprop_of th2b))
     val i2 = Thm.implies_elim i1 th1b
     val i3 = Thm.implies_intr (Thm.cprop_of th2b) i2
@@ -119,102 +108,115 @@
 
 fun conj1 th =
   let
-    val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th)))
-    val i = Thm.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct1}
+    val (P, Q) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th))
+    val i = Thm.instantiate' [] [SOME P, SOME Q] @{thm conjunct1}
   in
     meta_mp i th
   end
 
 fun conj2 th =
   let
-    val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th)))
-    val i = Thm.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct2}
+    val (P, Q) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th))
+    val i = Thm.instantiate' [] [SOME P, SOME Q] @{thm conjunct2}
   in
     meta_mp i th
   end
 
-fun refl ctm =
-  let
-    val cty = Thm.ctyp_of_cterm ctm
-  in
-    Thm.instantiate' [SOME cty] [SOME ctm] @{thm refl}
-  end
+fun refl t =
+  let val A = Thm.ctyp_of_cterm t
+  in Thm.instantiate' [SOME A] [SOME t] @{thm refl} end
 
-fun abs cv th =
+fun abs x th =
   let
     val th1 = implies_elim_all th
-    val (tl, tr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th1)))
-    val (ll, lr) = (Thm.lambda cv tl, Thm.lambda cv tr)
-    val (al, ar) = (Thm.apply ll cv, Thm.apply lr cv)
+    val (tl, tr) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th1))
+    val (f, g) = (Thm.lambda x tl, Thm.lambda x tr)
+    val (al, ar) = (Thm.apply f x, Thm.apply g x)
     val bl = beta al
     val br = meta_eq_to_obj_eq (Thm.symmetric (Thm.beta_conversion false ar))
-    val th2 = trans (trans bl th1) br
-    val th3 = implies_elim_all th2
-    val th4 = Thm.forall_intr cv th3
-    val i = Thm.instantiate' [SOME (Thm.ctyp_of_cterm cv), SOME (Thm.ctyp_of_cterm tl)]
-      [SOME ll, SOME lr] @{thm ext2}
+    val th2 =
+      trans (trans bl th1) br
+      |> implies_elim_all
+      |> Thm.forall_intr x
+    val i =
+      Thm.instantiate' [SOME (Thm.ctyp_of_cterm x), SOME (Thm.ctyp_of_cterm tl)]
+        [SOME f, SOME g] @{lemma "(\<And>x. f x = g x) \<Longrightarrow> f = g" by (rule ext)}
   in
-    meta_mp i th4
+    meta_mp i th2
   end
 
-fun freezeT thy thm =
+fun freezeT thy th =
   let
-    val tvars = Term.add_tvars (Thm.prop_of thm) []
-    val tfrees = map (fn ((t, _), s) => TFree (t, s)) tvars
+    fun add (v as ((a, _), S)) tvars =
+      if TVars.defined tvars v then tvars
+      else TVars.add (v, Thm.global_ctyp_of thy (TFree (a, S))) tvars
+    val tyinst =
+      TVars.build (Thm.prop_of th |> (fold_types o fold_atyps) (fn TVar v => add v | _ => I))
   in
-    Thm.instantiate (TVars.make (tvars ~~ map (Thm.global_ctyp_of thy) tfrees), Vars.empty) thm
+    Thm.instantiate (tyinst, Vars.empty) th
   end
 
-fun def' constname rhs thy =
+fun freeze thy = freezeT thy #> (fn th =>
   let
-    val rhs = Thm.term_of rhs
-    val typ = type_of rhs
-    val constbinding = Binding.name constname
-    val thy1 = Sign.add_consts [(constbinding, typ, NoSyn)] thy
-    val eq = Logic.mk_equals (Const (Sign.full_name thy1 constbinding, typ), rhs)
-    val (thm, thy2) = Global_Theory.add_def (Binding.suffix_name "_hldef" constbinding, eq) thy1
-    val def_thm = freezeT thy1 thm
+    val vars = Vars.build (th |> Thm.add_vars)
+    val inst = vars |> Vars.map (fn _ => fn v =>
+      let
+        val Var ((x, _), _) = Thm.term_of v
+        val ty = Thm.ctyp_of_cterm v
+      in Thm.free (x, ty) end)
+  in
+    Thm.instantiate (TVars.empty, inst) th
+  end)
+
+fun def' c rhs thy =
+  let
+    val b = Binding.name c
+    val ty = type_of rhs
+    val thy1 = Sign.add_consts [(b, ty, NoSyn)] thy
+    val eq = Logic.mk_equals (Const (Sign.full_name thy1 b, ty), rhs)
+    val (th, thy2) = Global_Theory.add_def (Binding.suffix_name "_hldef" b, eq) thy1
+    val def_thm = freezeT thy1 th
   in
     (meta_eq_to_obj_eq def_thm, thy2)
   end
 
-fun mdef name thy =
-  case Import_Data.get_const_def name thy of
+fun mdef thy name =
+  (case Import_Data.get_const_def thy name of
     SOME th => th
-  | NONE => error ("constant mapped but no definition: " ^ name)
+  | NONE => error ("Constant mapped, but no definition: " ^ quote name))
+
+fun def c rhs thy =
+  if is_some (Import_Data.get_const_def thy c) then
+    (warning ("Const mapped, but def provided: " ^ quote c); (mdef thy c, thy))
+  else def' c (Thm.term_of rhs) thy
 
-fun def constname rhs thy =
-  case Import_Data.get_const_def constname thy of
-    SOME _ =>
-      let
-        val () = warning ("Const mapped but def provided: " ^ constname)
-      in
-        (mdef constname thy, thy)
-      end
-  | NONE => def' constname rhs thy
+fun typedef_hol2hollight A B rep abs pred a r =
+  Thm.instantiate' [SOME A, SOME B] [SOME rep, SOME abs, SOME pred, SOME a, SOME r]
+    @{lemma "type_definition Rep Abs (Collect P) \<Longrightarrow> Abs (Rep a) = a \<and> P r = (Rep (Abs r) = r)"
+        by (metis type_definition.Rep_inverse type_definition.Abs_inverse
+              type_definition.Rep mem_Collect_eq)}
 
-fun typedef_hollight th thy =
+fun typedef_hollight th =
   let
-    val (th_s, cn) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
-    val (th_s, abst) = Thm.dest_comb th_s
-    val rept = Thm.dest_arg th_s
-    val P = Thm.dest_arg cn
-    val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
+    val ((rep, abs), P) =
+      Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
+      |>> (Thm.dest_comb #>> Thm.dest_arg)
+      ||> Thm.dest_arg
+    val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm rep)
   in
-    Thm.instantiate' [SOME nty, SOME oty] [SOME rept, SOME abst, SOME P,
-      SOME (Thm.global_cterm_of thy (Free ("a", Thm.typ_of nty))),
-      SOME (Thm.global_cterm_of thy (Free ("r", Thm.typ_of oty)))] @{thm typedef_hol2hollight}
+    typedef_hol2hollight A B rep abs P (Thm.free ("a", A)) (Thm.free ("r", B))
   end
 
 fun tydef' tycname abs_name rep_name cP ct td_th thy =
   let
     val ctT = Thm.ctyp_of_cterm ct
-    val nonempty = Thm.instantiate' [SOME ctT] [SOME cP, SOME ct] @{thm light_ex_imp_nonempty}
+    val nonempty = Thm.instantiate' [SOME ctT] [SOME cP, SOME ct]
+      @{lemma "P t \<Longrightarrow> \<exists>x. x \<in> Collect P" by auto}
     val th2 = meta_mp nonempty td_th
     val c =
-      case Thm.concl_of th2 of
-        _ $ (Const(\<^const_name>\<open>Ex\<close>,_) $ Abs(_,_,Const(\<^const_name>\<open>Set.member\<close>,_) $ _ $ c)) => c
-      | _ => error "type_introduction: bad type definition theorem"
+      (case Thm.concl_of th2 of
+        \<^Const_>\<open>Trueprop for \<^Const_>\<open>Ex _ for \<open>Abs (_, _, \<^Const_>\<open>Set.member _ for _ c\<close>)\<close>\<close>\<close> => c
+      | _ => raise THM ("type_introduction: bad type definition theorem", 0, [th2]))
     val tfrees = Term.add_tfrees c []
     val tnames = sort_strings (map fst tfrees)
     val typedef_bindings =
@@ -226,54 +228,33 @@
      (Typedef.add_typedef {overloaded = false}
        (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
        (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1)) thy
-    val aty = #abs_type (#1 typedef_info)
+    val aty = Thm.global_ctyp_of thy' (#abs_type (#1 typedef_info))
     val th = freezeT thy' (#type_definition (#2 typedef_info))
-    val (th_s, _) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
-    val (th_s, abst) = Thm.dest_comb th_s
-    val rept = Thm.dest_arg th_s
-    val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
-    val typedef_th =
-       Thm.instantiate'
-          [SOME nty, SOME oty]
-          [SOME rept, SOME abst, SOME cP, SOME (Thm.global_cterm_of thy' (Free ("a", aty))),
-             SOME (Thm.global_cterm_of thy' (Free ("r", Thm.typ_of ctT)))]
-          @{thm typedef_hol2hollight}
-    val th4 = typedef_th OF [#type_definition (#2 typedef_info)]
+    val (rep, abs) =
+      Thm.dest_comb (#1 (Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th)))) |>> Thm.dest_arg
+    val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm rep)
+    val typedef_th = typedef_hol2hollight A B rep abs cP (Thm.free ("a", aty)) (Thm.free ("r", ctT))
   in
-    (th4, thy')
+    (typedef_th OF [#type_definition (#2 typedef_info)], thy')
   end
 
-fun mtydef name thy =
-  case Import_Data.get_typ_def name thy of
-    SOME thn => meta_mp (typedef_hollight thn thy) thn
-  | NONE => error ("type mapped but no tydef thm registered: " ^ name)
+fun mtydef thy name =
+  (case Import_Data.get_typ_def thy name of
+    SOME th => meta_mp (typedef_hollight th) th
+  | NONE => error ("Type mapped, but no tydef thm registered: " ^ quote name))
 
 fun tydef tycname abs_name rep_name P t td_th thy =
-  case Import_Data.get_typ_def tycname thy of
-    SOME _ =>
-      let
-        val () = warning ("Type mapped but proofs provided: " ^ tycname)
-      in
-        (mtydef tycname thy, thy)
-      end
-  | NONE => tydef' tycname abs_name rep_name P t td_th thy
+  if is_some (Import_Data.get_typ_def thy tycname) then
+    (warning ("Type mapped but proofs provided: " ^ quote tycname); (mtydef thy tycname, thy))
+  else tydef' tycname abs_name rep_name P t td_th thy
 
-fun inst_type lambda th thy =
+fun inst_type lambda =
   let
-    fun assoc _ [] = error "assoc"
-      | assoc x ((x',y)::rest) = if x = x' then y else assoc x rest
-    val lambda = map (fn (a, b) => (Thm.typ_of a, b)) lambda
-    val tys_before = Term.add_tfrees (Thm.prop_of th) []
-    val th1 = Thm.varifyT_global th
-    val tys_after = Term.add_tvars (Thm.prop_of th1) []
     val tyinst =
-      map2 (fn bef => fn iS =>
-        (case try (assoc (TFree bef)) lambda of
-          SOME cty => (iS, cty)
-        | NONE => (iS, Thm.global_ctyp_of thy (TFree bef))))
-      tys_before tys_after
+      TFrees.build (lambda |> fold (fn (a, b) =>
+        TFrees.add (Term.dest_TFree (Thm.typ_of a), b)))
   in
-    Thm.instantiate (TVars.make tyinst, Vars.empty) th1
+    Thm.instantiate_frees (tyinst, Frees.empty)
   end
 
 fun inst sigma th =
@@ -284,167 +265,181 @@
        |> forall_elim_list rng
   end
 
-fun transl_dotc #"." = "dot"
-  | transl_dotc c = Char.toString c
-val transl_dot = String.translate transl_dotc
+val make_name = String.translate (fn #"." => "dot" | c => Char.toString c)
+
+fun make_free (x, ty) = Free (make_name x, ty)
 
-fun transl_qmc #"?" = "t"
-  | transl_qmc c = Char.toString c
-val transl_qm = String.translate transl_qmc
+fun make_tfree a =
+  let val b = "'" ^ String.translate (fn #"?" => "t" | c => Char.toString c) a
+  in TFree (b, \<^sort>\<open>type\<close>) end
 
-fun getconstname s thy =
-  case Import_Data.get_const_map s thy of
-      SOME s => s
-    | NONE => Sign.full_name thy (Binding.name (transl_dot s))
-fun gettyname s thy =
-  case Import_Data.get_typ_map s thy of
-    SOME s => s
-  | NONE => Sign.full_name thy (Binding.name s)
+fun make_type thy (c, args) =
+  let
+    val d =
+      (case Import_Data.get_typ_map thy c of
+        SOME d => d
+      | NONE => Sign.full_bname thy (make_name c))
+  in Type (d, args) end
+
+fun make_const thy (c, ty) =
+  let
+    val d =
+      (case Import_Data.get_const_map thy c of
+        SOME d => d
+      | NONE => Sign.full_bname thy (make_name c))
+  in Const (d, ty) end
+
+
+datatype state =
+  State of theory * (ctyp Inttab.table * int) * (cterm Inttab.table * int) * (thm Inttab.table * int)
+
+fun init_state thy = State (thy, (Inttab.empty, 0), (Inttab.empty, 0), (Inttab.empty, 0))
 
-fun get (map, no) s =
-  case Int.fromString s of
-    NONE => error "Import_Rule.get: not a number"
-  | SOME i => (case Inttab.lookup map (Int.abs i) of
-      NONE => error "Import_Rule.get: lookup failed"
-    | SOME res => (res, (if i < 0 then Inttab.delete (Int.abs i) map else map, no)))
+fun get (tab, no) s =
+  (case Int.fromString s of
+    NONE => raise Fail "get: not a number"
+  | SOME i =>
+      (case Inttab.lookup tab (Int.abs i) of
+        NONE => raise Fail "get: lookup failed"
+      | SOME res => (res, (if i < 0 then Inttab.delete (Int.abs i) tab else tab, no))))
 
-fun getty i (thy, (tyi, tmi, thi)) = let val (i, tyi) = (get tyi i) in (i, (thy, (tyi, tmi, thi))) end
-fun gettm i (thy, (tyi, tmi, thi)) = let val (i, tmi) = (get tmi i) in (i, (thy, (tyi, tmi, thi))) end
-fun getth i (thy, (tyi, tmi, thi)) = let val (i, thi) = (get thi i) in (i, (thy, (tyi, tmi, thi))) end
-fun set (map, no) v = (Inttab.update_new (no + 1, v) map, no + 1)
-fun setty v (thy, (tyi, tmi, thi)) = (thy, (set tyi v, tmi, thi))
-fun settm v (thy, (tyi, tmi, thi)) = (thy, (tyi, set tmi v, thi))
-fun setth v (thy, (tyi, tmi, thi)) = (thy, (tyi, tmi, set thi v))
+fun get_theory (State (thy, _, _, _)) = thy;
+fun map_theory f (State (thy, a, b, c)) = State (f thy, a, b, c);
+fun map_theory_result f (State (thy, a, b, c)) =
+  let val (res, thy') = f thy in (res, State (thy', a, b, c)) end;
+
+fun ctyp_of (State (thy, _, _, _)) = Thm.global_ctyp_of thy;
+fun cterm_of (State (thy, _, _, _)) = Thm.global_cterm_of thy;
+
+fun typ i (State (thy, a, b, c)) = let val (i, a') = get a i in (i, State (thy, a', b, c)) end
+fun term i (State (thy, a, b, c)) = let val (i, b') = get b i in (i, State (thy, a, b', c)) end
+fun thm i (State (thy, a, b, c)) = let val (i, c') = get c i in (i, State (thy, a, b, c')) end
 
-fun last_thm (_, _, (map, no)) =
-  case Inttab.lookup map no of
-    NONE => error "Import_Rule.last_thm: lookup failed"
-  | SOME thm => thm
+fun set (tab, no) v = (Inttab.update_new (no + 1, v) tab, no + 1)
+fun set_typ ty (State (thy, a, b, c)) = State (thy, set a ty, b, c)
+fun set_term tm (State (thy, a, b, c)) = State (thy, a, set b tm, c)
+fun set_thm th (State (thy, a, b, c)) = State (thy, a, b, set c th)
+
+fun last_thm (State (_, _, _, (tab, no))) =
+  case Inttab.lookup tab no of
+    NONE => raise Fail "last_thm: lookup failed"
+  | SOME th => th
 
-fun listLast (h1 :: (h2 :: t)) = apfst (fn t => h1 :: h2 :: t) (listLast t)
-  | listLast [p] = ([], p)
-  | listLast [] = error "listLast: empty"
+fun list_last (x :: y :: zs) = apfst (fn t => x :: y :: t) (list_last zs)
+  | list_last [x] = ([], x)
+  | list_last [] = raise Fail "list_last: empty"
 
-fun pairList (h1 :: (h2 :: t)) = ((h1, h2) :: pairList t)
-  | pairList [] = []
-  | pairList _ = error "pairList: odd list length"
+fun pair_list (x :: y :: zs) = ((x, y) :: pair_list zs)
+  | pair_list [] = []
+  | pair_list _ = raise Fail "pair_list: odd list length"
 
-fun store_thm binding thm thy =
+fun store_thm binding th0 thy =
   let
     val ctxt = Proof_Context.init_global thy
-    val thm = Drule.export_without_context_open thm
-    val tvs = Term.add_tvars (Thm.prop_of thm) []
+    val th = Drule.export_without_context_open th0
+    val tvs = Term.add_tvars (Thm.prop_of th) []
     val tns = map (fn (_, _) => "'") tvs
     val nms = Name.variants (Variable.names_of ctxt) tns
     val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs))
-    val thm' = Thm.instantiate (TVars.make (tvs ~~ map (Thm.ctyp_of ctxt) vs), Vars.empty) thm
+    val th' = Thm.instantiate (TVars.make (tvs ~~ map (Thm.ctyp_of ctxt) vs), Vars.empty) th
   in
-    snd (Global_Theory.add_thm ((binding, thm'), []) thy)
-  end
-
-fun log_timestamp () =
-  let
-    val time = Time.now ()
-    val millis = nth (space_explode "." (Time.fmt 3 time)) 1
-  in
-    Date.fmt "%d.%m.%Y %H:%M:%S." (Date.fromTimeLocal time) ^ millis
+    snd (Global_Theory.add_thm ((binding, th'), []) thy)
   end
 
-fun process_line str tstate =
+fun parse_line s =
+  (case String.tokens (fn x => x = #"\n" orelse x = #" ") s of
+    [] => raise Fail "parse_line: empty"
+  | cmd :: args =>
+      (case String.explode cmd of
+        [] => raise Fail "parse_line: empty command"
+      | c :: cs => (c, String.implode cs :: args)))
+
+fun process_line str =
   let
-    fun process tstate (#"R", [t]) = gettm t tstate |>> refl |-> setth
-      | process tstate (#"B", [t]) = gettm t tstate |>> beta |-> setth
-      | process tstate (#"1", [th]) = getth th tstate |>> conj1 |-> setth
-      | process tstate (#"2", [th]) = getth th tstate |>> conj2 |-> setth
-      | process tstate (#"H", [t]) =
-          gettm t tstate |>> Thm.apply \<^cterm>\<open>Trueprop\<close> |>> Thm.trivial |-> setth
-      | process tstate (#"A", [_, t]) =
-          gettm t tstate |>> Thm.apply \<^cterm>\<open>Trueprop\<close> |>> Skip_Proof.make_thm_cterm |-> setth
-      | process tstate (#"C", [th1, th2]) =
-          getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => comb t1 t2) |-> setth
-      | process tstate (#"T", [th1, th2]) =
-          getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => trans t1 t2) |-> setth
-      | process tstate (#"E", [th1, th2]) =
-          getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => eq_mp t1 t2) |-> setth
-      | process tstate (#"D", [th1, th2]) =
-          getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => deduct t1 t2) |-> setth
-      | process tstate (#"L", [t, th]) =
-          gettm t tstate ||>> (fn ti => getth th ti) |>> (fn (tm, th) => abs tm th) |-> setth
-      | process (thy, state) (#"M", [s]) =
+    fun process (#"R", [t]) = term t #>> refl #-> set_thm
+      | process (#"B", [t]) = term t #>> beta #-> set_thm
+      | process (#"1", [th]) = thm th #>> conj1 #-> set_thm
+      | process (#"2", [th]) = thm th #>> conj2 #-> set_thm
+      | process (#"H", [t]) = term t #>> Thm.apply \<^cterm>\<open>Trueprop\<close> #>> Thm.trivial #-> set_thm
+      | process (#"A", [_, t]) =
+          term t #>> Thm.apply \<^cterm>\<open>Trueprop\<close> #>> Skip_Proof.make_thm_cterm #-> set_thm
+      | process (#"C", [th1, th2]) = thm th1 ##>> thm th2 #>> uncurry comb #-> set_thm
+      | process (#"T", [th1, th2]) = thm th1 ##>> thm th2 #>> uncurry trans #-> set_thm
+      | process (#"E", [th1, th2]) = thm th1 ##>> thm th2 #>> uncurry eq_mp #-> set_thm
+      | process (#"D", [th1, th2]) = thm th1 ##>> thm th2 #>> uncurry deduct #-> set_thm
+      | process (#"L", [t, th]) = term t ##>> (fn ti => thm th ti) #>> uncurry abs #-> set_thm
+      | process (#"M", [s]) = (fn state =>
           let
-            val ctxt = Proof_Context.init_global thy
-            val thm = freezeT thy (Global_Theory.get_thm thy s)
-            val ((_, [th']), _) = Variable.import true [thm] ctxt
+            val thy = get_theory state
+            val th = Global_Theory.get_thm thy s
           in
-            setth th' (thy, state)
-          end
-      | process (thy, state) (#"Q", l) =
+            set_thm (freeze thy th) state
+          end)
+      | process (#"Q", l) = (fn state =>
           let
-            val (tys, th) = listLast l
-            val (th, tstate) = getth th (thy, state)
-            val (tys, tstate) = fold_map getty tys tstate
-          in
-            setth (inst_type (pairList tys) th thy) tstate
-          end
-      | process tstate (#"S", l) =
-          let
-            val (tms, th) = listLast l
-            val (th, tstate) = getth th tstate
-            val (tms, tstate) = fold_map gettm tms tstate
+            val (tys, th) = list_last l
+            val (th, state1) = thm th state
+            val (tys, state2) = fold_map typ tys state1
           in
-            setth (inst (pairList tms) th) tstate
-          end
-      | process tstate (#"F", [name, t]) =
+            set_thm (inst_type (pair_list tys) th) state2
+          end)
+      | process (#"S", l) = (fn state =>
           let
-            val (tm, (thy, state)) = gettm t tstate
-            val (th, thy) = def (transl_dot name) tm thy
+            val (tms, th) = list_last l
+            val (th, state1) = thm th state
+            val (tms, state2) = fold_map term tms state1
           in
-            setth th (thy, state)
-          end
-      | process (thy, state) (#"F", [name]) = setth (mdef name thy) (thy, state)
-      | process tstate (#"Y", [name, absname, repname, t1, t2, th]) =
+            set_thm (inst (pair_list tms) th) state2
+          end)
+      | process (#"F", [name, t]) = (fn state =>
           let
-            val (th, tstate) = getth th tstate
-            val (t1, tstate) = gettm t1 tstate
-            val (t2, (thy, state)) = gettm t2 tstate
-            val (th, thy) = tydef name absname repname t1 t2 th thy
+            val (tm, state1) = term t state
           in
-            setth th (thy, state)
-          end
-      | process (thy, state) (#"Y", [name, _, _]) = setth (mtydef name thy) (thy, state)
-      | process (thy, state) (#"t", [n]) =
-          setty (Thm.global_ctyp_of thy (TFree ("'" ^ (transl_qm n), \<^sort>\<open>type\<close>))) (thy, state)
-      | process (thy, state) (#"a", n :: l) =
-          fold_map getty l (thy, state) |>>
-            (fn tys => Thm.global_ctyp_of thy (Type (gettyname n thy, map Thm.typ_of tys))) |-> setty
-      | process (thy, state) (#"v", [n, ty]) =
-          getty ty (thy, state) |>> (fn ty => Thm.global_cterm_of thy (Free (transl_dot n, Thm.typ_of ty))) |-> settm
-      | process (thy, state) (#"c", [n, ty]) =
-          getty ty (thy, state) |>> (fn ty => Thm.global_cterm_of thy (Const (getconstname n thy, Thm.typ_of ty))) |-> settm
-      | process tstate (#"f", [t1, t2]) =
-          gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.apply t1 t2) |-> settm
-      | process tstate (#"l", [t1, t2]) =
-          gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.lambda t1 t2) |-> settm
-      | process (thy, state) (#"+", [s]) =
-          (store_thm (Binding.name (transl_dot s)) (last_thm state) thy, state)
-      | process _ (c, _) = error ("process: unknown command: " ^ String.implode [c])
-
-    fun parse_line s =
-        case String.tokens (fn x => (x = #"\n" orelse x = #" ")) s of
-          [] => error "parse_line: empty"
-        | h :: t => (case String.explode h of
-            [] => error "parse_line: empty command"
-          | sh :: st => (sh, (String.implode st) :: t))
+            state1
+            |> map_theory_result (def (make_name name) tm)
+            |-> set_thm
+          end)
+      | process (#"F", [name]) = (fn state => set_thm (mdef (get_theory state) name) state)
+      | process (#"Y", [name, absname, repname, t1, t2, th]) = (fn state =>
+          let
+            val (th, state1) = thm th state
+            val (t1, state2) = term t1 state1
+            val (t2, state3) = term t2 state2
+          in
+            state3
+            |> map_theory_result (tydef name absname repname t1 t2 th)
+            |-> set_thm
+          end)
+      | process (#"Y", [name, _, _]) = (fn state => set_thm (mtydef (get_theory state) name) state)
+      | process (#"t", [n]) = (fn state => set_typ (ctyp_of state (make_tfree n)) state)
+      | process (#"a", n :: l) = (fn state =>
+          fold_map typ l state
+          |>> (fn tys => ctyp_of state (make_type (get_theory state) (n, map Thm.typ_of tys)))
+          |-> set_typ)
+      | process (#"v", [n, ty]) = (fn state =>
+          typ ty state |>> (fn ty => cterm_of state (make_free (n, Thm.typ_of ty))) |-> set_term)
+      | process (#"c", [n, ty]) = (fn state =>
+          typ ty state |>> (fn ty =>
+            cterm_of state (make_const (get_theory state) (n, Thm.typ_of ty))) |-> set_term)
+      | process (#"f", [t1, t2]) = term t1 ##>> term t2 #>> uncurry Thm.apply #-> set_term
+      | process (#"l", [t1, t2]) = term t1 ##>> term t2 #>> uncurry Thm.lambda #-> set_term
+      | process (#"+", [s]) = (fn state =>
+          map_theory (store_thm (Binding.name (make_name s)) (last_thm state)) state)
+      | process (c, _) = raise Fail ("process: unknown command: " ^ String.str c)
   in
-    process tstate (parse_line str)
+    process (parse_line str)
   end
 
-fun process_file path thy =
-  #1 (fold process_line (File.read_lines path) (thy, init_state))
+fun import_file path0 thy =
+  let
+    val path = File.absolute_path (Resources.master_directory thy + path0)
+    val lines =
+      if Path.is_zst path then Bytes.read path |> Zstd.uncompress |> Bytes.trim_split_lines
+      else File.read_lines path
+  in get_theory (fold process_line lines (init_state thy)) end
 
-val _ = Outer_Syntax.command \<^command_keyword>\<open>import_file\<close>
-  "import a recorded proof file"
-  (Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))
-
+val _ =
+  Outer_Syntax.command \<^command_keyword>\<open>import_file\<close> "import recorded proofs from HOL Light"
+    (Parse.path >> (fn name => Toplevel.theory (fn thy => import_file (Path.explode name) thy)))
 
 end
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/HOL/Library/code_test.ML	Fri Jan 17 23:00:13 2025 +0000
@@ -426,7 +426,7 @@
     val _ = List.app (File.write code_path o snd) code_files
     val _ = File.write driver_path driver
     val cmd =
-      "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg" ^
+      "\"$ISABELLE_OCAMLFIND\" ocamlopt -w -p-u -package zarith -linkpkg" ^
       " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path dir ^ " " ^
       File.bash_path code_path ^ " " ^ File.bash_path driver_path ^ " </dev/null"
   in compile compiler cmd; evaluate compiler (File.bash_path compiled_path) end
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/HOL/ROOT	Fri Jan 17 23:00:13 2025 +0000
@@ -374,11 +374,12 @@
     Generate_Target_Nat
     Generate_Abstract_Char
     Generate_Efficient_Datastructures
-    Generate_Target_String_Literals
-    Generate_Target_Bit_Operations
     Code_Lazy_Test
     Code_Test_PolyML
     Code_Test_Scala
+  theories [condition = "ISABELLE_GHC,ISABELLE_OCAMLFIND"]
+    Generate_Target_String_Literals
+    Generate_Target_Bit_Operations
   theories [condition = ISABELLE_GHC]
     Code_Test_GHC
   theories [condition = ISABELLE_MLTON]
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Fri Jan 17 23:00:13 2025 +0000
@@ -13,7 +13,7 @@
     val ([{src_path, lines = vc_lines, pos = vc_pos, ...}: Token.file,
       {lines = fdl_lines, pos = fdl_pos, ...},
       {lines = rls_lines, pos = rls_pos, ...}], thy') = files thy;
-    val path = fst (Path.split_ext src_path);
+    val path = Path.drop_ext src_path;
   in
     SPARK_VCs.set_vcs
       (snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines)))
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/Pure/Admin/component_hol_light.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/component_hol_light.scala	Fri Jan 17 23:00:13 2025 +0000
@@ -0,0 +1,268 @@
+/*  Title:      Pure/Admin/component_hol_light.scala
+    Author:     Makarius
+
+Build component for HOL-Light, with export of facts and proofs, offline
+optimization, and import to Isabelle/HOL.
+*/
+
+package isabelle
+
+
+object Component_HOL_Light {
+  /* resources */
+
+  val default_hol_light_url = "https://github.com/jrh13/hol-light.git"
+  val default_hol_light_rev = "Release-3.0.0"
+
+  val default_hol_light_patched_url = "https://gitlab.inria.fr/hol-light-isabelle/hol-light.git"
+  val default_hol_light_patched_rev = "master"
+
+  val default_import_url = "https://gitlab.inria.fr/hol-light-isabelle/import.git"
+  val default_import_rev = "master"
+
+  def hol_light_dirs(base_dir: Path): (Path, Path) =
+    (base_dir + Path.basic("hol-light"), base_dir + Path.basic("hol-light-patched"))
+
+  val patched_files: List[Path] =
+    List("fusion.ml", "statements.ml", "stage1.ml", "stage2.ml").map(Path.explode)
+
+  def make_patch(base_dir: Path): String = {
+    val (dir1, dir2) = hol_light_dirs(Path.current)
+    (for (path <- patched_files) yield {
+      val path1 = dir1 + path
+      val path2 = dir2 + path
+      if ((base_dir + path1).is_file || (base_dir + path2).is_file) {
+        Isabelle_System.make_patch(base_dir, path1, path2)
+      }
+      else ""
+    }).mkString
+  }
+
+  def build_hol_light_import(
+    only_offline: Boolean = false,
+    progress: Progress = new Progress,
+    target_dir: Path = Path.current,
+    hol_light_url: String = default_hol_light_url,
+    hol_light_rev: String = default_hol_light_rev,
+    hol_light_patched_url: String = default_hol_light_patched_url,
+    hol_light_patched_rev: String = default_hol_light_patched_rev,
+    import_url: String = default_import_url,
+    import_rev: String = default_import_rev
+  ): Unit = {
+    /* system */
+
+    if (!only_offline) {
+      Linux.check_system()
+      Isabelle_System.require_command("buffer", test = "-i /dev/null")
+      Isabelle_System.require_command("patch")
+    }
+
+
+    /* component */
+
+    val component_name = "hol_light_import-" + Date.Format.alt_date(Date.now())
+    val component_dir = Components.Directory(target_dir + Path.basic(component_name)).create()
+
+    val platform = Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true, apple = true)
+    val platform_dir = Isabelle_System.make_directory(component_dir.path + Path.basic(platform))
+
+
+    /* settings */
+
+    component_dir.write_settings("""
+HOL_LIGHT_IMPORT="$COMPONENT"
+HOL_LIGTH_BUNDLE="$HOL_LIGHT_IMPORT/bundle/proofs"
+HOL_LIGHT_OFFLINE="$HOL_LIGHT_IMPORT/${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}/offline"
+""")
+
+
+    /* README */
+
+    File.write(component_dir.README,
+      """Author: Cezary Kaliszyk, University of Innsbruck, 2013
+Author: Alexander Krauss, QAware GmbH, 2013
+Author: Sophie Tourret, INRIA, 2024
+Author: Stéphane Glondu, INRIA, 2024
+LICENSE (export tools): BSD-3 from Isabelle
+LICENSE (HOL Light proofs): BSD-2 from HOL Light
+
+
+This is an export of primitive proofs from HOL Light """ + hol_light_rev + """.
+
+The original repository """ + hol_light_url + """
+has been patched in 2 stages. The overall export process works like this:
+
+  make
+
+  patch -p1 < patches/stage1.patch
+  ./ocaml-hol -I +compiler-libs stage1.ml
+
+  patch -p1 < patches/stage2.patch
+  export MAXTMS=10000
+  ./ocaml-hol -I +compiler-libs stage2.ml
+
+  gzip -d proofs.gz
+  > maps.lst
+  x86_64-linux/offline
+
+
+      Makarius
+      """ + Date.Format.date(Date.now()) + "\n")
+
+
+    Isabelle_System.with_tmp_dir("build") { tmp_dir =>
+
+      /* OCaml setup */
+
+      progress.echo("Setup OCaml ...")
+
+      progress.bash(
+        if (only_offline) "isabelle ocaml_setup_base"
+        else "isabelle ocaml_setup && isabelle ocaml_opam install -y camlp5",
+        echo = progress.verbose).check
+
+      val opam_env = Isabelle_System.bash("isabelle ocaml_opam env").check.out
+
+
+      /* repository clones */
+
+      val (hol_light_dir, hol_light_patched_dir) = hol_light_dirs(tmp_dir)
+      val import_dir = tmp_dir + Path.basic("import")
+
+      if (!only_offline) {
+        Isabelle_System.git_clone(hol_light_url, hol_light_dir, checkout = hol_light_rev,
+          progress = progress)
+
+        Isabelle_System.git_clone(
+          hol_light_patched_url, hol_light_patched_dir, checkout = hol_light_patched_rev,
+          progress = progress)
+      }
+
+      Isabelle_System.git_clone(import_url, import_dir, checkout = import_rev, progress = progress)
+
+
+      /* "offline" tool */
+
+      progress.echo("Building offline tool ...")
+
+      val offline_path = Path.explode("offline")
+      val offline_exe = offline_path.platform_exe
+      val import_offline_dir = import_dir + offline_path
+
+      Isabelle_System.copy_dir(import_offline_dir, component_dir.path)
+      (component_dir.path + Path.explode("offline/.gitignore")).file.delete
+
+      progress.bash("make", cwd = import_offline_dir, echo = progress.verbose).check
+      Isabelle_System.copy_file(import_offline_dir + offline_exe, platform_dir + offline_exe)
+      File.set_executable(platform_dir + offline_exe)
+
+
+      if (!only_offline) {
+
+        /* patches */
+
+        progress.echo("Preparing patches ...")
+
+        val patches_dir = Isabelle_System.make_directory(component_dir.path + Path.basic("patches"))
+        val patch1 = patches_dir + Path.basic("stage1.patch")
+        val patch2 = patches_dir + Path.basic("stage2.patch")
+
+        Isabelle_System.bash("git reset --hard origin/stdlib/isabelle-export-base",
+          cwd = hol_light_patched_dir).check
+
+        File.write(patch1, make_patch(tmp_dir))
+
+        Isabelle_System.bash("patch -p1 < " + File.bash_path(patch1), cwd = hol_light_dir).check
+
+        Isabelle_System.bash("git reset --hard origin/stdlib/isabelle-export",
+          cwd = hol_light_patched_dir).check
+
+        File.write(patch2, make_patch(tmp_dir))
+
+
+        /* export */
+
+        progress.echo("Exporting proofs ...")
+        progress.bash(
+          Library.make_lines("set -e", opam_env,
+            "make",
+            "./ocaml-hol -I +compiler-libs stage1.ml",
+            "patch -p1 < " + File.bash_path(patch2),
+            "export MAXTMS=10000",
+            "./ocaml-hol -I +compiler-libs stage2.ml",
+            "gzip -d proofs.gz",
+            "> maps.lst",
+            File.bash_path(platform_dir + offline_exe) + " proofs"
+          ),
+          cwd = hol_light_dir, echo = progress.verbose).check
+
+        val bundle_dir = Isabelle_System.make_directory(component_dir.path + Path.explode("bundle"))
+        Isabelle_System.copy_file(hol_light_dir + Path.explode("proofs"), bundle_dir)
+      }
+    }
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("component_hol_light_import", "build Isabelle component for HOL Light import",
+      Scala_Project.here,
+      { args =>
+        var target_dir = Path.current
+        var only_offline = false
+        var hol_light_url = default_hol_light_url
+        var hol_light_patched_url = default_hol_light_patched_url
+        var hol_light_rev = default_hol_light_rev
+        var hol_light_patched_rev = default_hol_light_patched_rev
+        var import_url = default_import_url
+        var import_rev = default_import_rev
+        var verbose = false
+
+        val getopts = Getopts("""
+Usage: isabelle component_hol_light_import [OPTIONS]
+
+  Options are:
+    -D DIR       target directory (default ".")
+    -O           only build the "offline" tool
+    -U URL       git URL for original HOL Light repository, default:
+                 """ + default_hol_light_url + """
+    -V URL       git URL for patched HOL Light repository, default:
+                 """ + default_hol_light_patched_url + """
+    -W URL       git URL for import repository, default:
+                 """ + default_import_url + """
+    -r REV       revision or branch to checkout HOL Light (default: """ +
+                    default_hol_light_rev + """)
+    -s REV       revision or branch to checkout HOL-Light-to-Isabelle (default: """ +
+                    default_hol_light_patched_rev + """)
+    -t REV       revision or branch to checkout import (default: """ +
+                    default_import_rev + """)
+    -v           verbose
+
+  Build Isabelle component for HOL Light import.
+""",
+          "D:" -> (arg => target_dir = Path.explode(arg)),
+          "O" -> (_ => only_offline = true),
+          "U:" -> (arg => hol_light_url = arg),
+          "V:" -> (arg => hol_light_patched_url = arg),
+          "W:" -> (arg => import_url = arg),
+          "r:" -> (arg => hol_light_rev = arg),
+          "s:" -> (arg => hol_light_patched_rev = arg),
+          "t:" -> (arg => import_rev = arg),
+          "v" -> (_ => verbose = true))
+
+        val more_args = getopts(args)
+        if (more_args.nonEmpty) getopts.usage()
+
+        val progress = new Console_Progress(verbose = verbose)
+
+        build_hol_light_import(
+          only_offline = only_offline, progress = progress, target_dir = target_dir,
+          hol_light_url = hol_light_url,
+          hol_light_rev = hol_light_rev,
+          hol_light_patched_url = hol_light_patched_url,
+          hol_light_patched_rev = hol_light_patched_rev,
+          import_url = import_url,
+          import_rev = import_rev)
+      })
+}
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/Pure/General/path.ML	Fri Jan 17 23:00:13 2025 +0000
@@ -33,7 +33,10 @@
   val ext: string -> T -> T
   val platform_exe: T -> T
   val split_ext: T -> T * string
-  val exe: T -> T
+  val drop_ext: T -> T
+  val get_ext: T -> string
+  val is_xz: T -> bool
+  val is_zst: T -> bool
   val expand: T -> T
   val file_name: T -> string
   eqtype binding
@@ -213,7 +216,11 @@
     ([], _) => (Path [Basic s], "")
   | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
 
-val exe = ML_System.platform_is_windows ? ext "exe";
+val drop_ext = #1 o split_ext;
+val get_ext = #2 o split_ext;
+
+fun is_xz path = get_ext path = "xz";
+fun is_zst path = get_ext path = "zst";
 
 
 (* expand variables *)
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/Pure/ROOT.ML	Fri Jan 17 23:00:13 2025 +0000
@@ -1,6 +1,6 @@
 (*  Title:      Pure/ROOT.ML
     Author:     Makarius
-    UUID:       b5c84e7e-c43b-4cf5-9644-a1f387b61ab4
+    UUID:       e075658d-0c3c-4076-892c-37ce2c40df8e
 
 Main entry point for the Isabelle/Pure bootstrap process.
 
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/Pure/System/isabelle_system.scala	Fri Jan 17 23:00:13 2025 +0000
@@ -495,13 +495,24 @@
   }
 
   def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {
-    with_tmp_file("patch") { patch =>
+    val lines =
       Isabelle_System.bash(
-        "diff -ru " + diff_options + " -- " + File.bash_path(src) + " " + File.bash_path(dst) +
-          " > " + File.bash_path(patch),
-        cwd = base_dir).check_rc(_ <= 1)
-      File.read(patch)
-    }
+        "diff -Nru" + if_proper(diff_options, " " + diff_options) + " -- " +
+          File.bash_path(src) + " " + File.bash_path(dst),
+        cwd = base_dir).check_rc(Process_Result.RC.regular).out_lines
+    Library.terminate_lines(lines)
+  }
+
+  def git_clone(url: String, target: Path,
+    checkout: String = "HEAD",
+    ssh: SSH.System = SSH.Local,
+    progress: Progress = new Progress
+  ): Unit = {
+    progress.echo("Cloning " + quote(url) + " ...")
+    bash(
+      "git clone --quiet --no-checkout " + Bash.string(url) + " . && " +
+      "git checkout --quiet --detach " + Bash.string(checkout),
+      ssh = ssh, cwd = ssh.make_directory(target)).check
   }
 
   def open(arg: String): Unit =
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/Pure/System/isabelle_tool.scala	Fri Jan 17 23:00:13 2025 +0000
@@ -180,6 +180,7 @@
   Component_Elm.isabelle_tool,
   Component_Foiltex.isabelle_tool,
   Component_Fonts.isabelle_tool,
+  Component_HOL_Light.isabelle_tool,
   Component_Hugo.isabelle_tool,
   Component_Javamail.isabelle_tool,
   Component_JCEF.isabelle_tool,
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/Pure/System/process_result.scala	Fri Jan 17 23:00:13 2025 +0000
@@ -18,6 +18,8 @@
     val interrupt = 130
     val timeout = 142
 
+    val regular: Set[Int] = Set(ok, error)
+
     private def text(rc: Int): String = {
       val txt =
         rc match {
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/Pure/Tools/generated_files.ML	Fri Jan 17 23:00:13 2025 +0000
@@ -253,7 +253,7 @@
 
     val (path, pos) = Path.dest_binding binding;
     val file_type =
-      get_file_type thy (#2 (Path.split_ext path))
+      get_file_type thy (Path.get_ext path)
         handle ERROR msg => error (msg ^ Position.here pos);
 
     val header = #make_comment file_type " generated by Isabelle ";
@@ -343,7 +343,8 @@
         export |> List.app (fn (bindings, executable) =>
           bindings |> List.app (fn binding0 =>
             let
-              val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe);
+              val binding = binding0
+                |> Path.map_binding (executable = SOME true ? Path.platform_exe);
               val (path, pos) = Path.dest_binding binding;
               val content =
                 (case try Bytes.read (dir + path) of
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/Pure/library.scala	Fri Jan 17 23:00:13 2025 +0000
@@ -147,6 +147,8 @@
   def cat_lines(lines: IterableOnce[String]): String =
     lines.iterator.mkString("\n")
 
+  def make_lines(lines: String*): String = cat_lines(lines)
+
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
   def prefix_lines(prfx: String, str: String): String =
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/Pure/thm.ML	Fri Jan 17 23:00:13 2025 +0000
@@ -49,6 +49,7 @@
   val dest_abs_fresh: string -> cterm -> cterm * cterm
   val dest_abs_global: cterm -> cterm * cterm
   val rename_tvar: indexname -> ctyp -> ctyp
+  val free: string * ctyp -> cterm
   val var: indexname * ctyp -> cterm
   val apply: cterm -> cterm -> cterm
   val lambda_name: string * cterm -> cterm -> cterm
@@ -340,6 +341,9 @@
     val _ = if i < 0 then raise TYPE ("rename_tvar: bad index", [TVar ((a, i), S)], []) else ();
   in Ctyp {cert = cert, T = TVar ((a, i), S), maxidx = Int.max (i, maxidx), sorts = sorts} end;
 
+fun free (x, Ctyp {cert, T, maxidx, sorts}) =
+  Cterm {cert = cert, t = Free (x, T), T = T, maxidx = maxidx, sorts = sorts};
+
 fun var ((x, i), Ctyp {cert, T, maxidx, sorts}) =
   if i < 0 then raise TERM ("var: bad index", [Var ((x, i), T)])
   else Cterm {cert = cert, t = Var ((x, i), T), T = T, maxidx = Int.max (i, maxidx), sorts = sorts};
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/Tools/Code/code_ml.ML	Fri Jan 17 23:00:13 2025 +0000
@@ -886,7 +886,7 @@
         make_destination = fn p => p + Path.explode "ROOT.ml"
           (*extension demanded by OCaml compiler*),
         make_command = fn _ =>
-          "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null"},
+          "\"$ISABELLE_OCAMLFIND\" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml </dev/null"},
       evaluation_args = []})
   #> Code_Target.set_printings (Type_Constructor ("fun",
     [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/Tools/VSCode/src/component_vscodium.scala
--- a/src/Tools/VSCode/src/component_vscodium.scala	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/Tools/VSCode/src/component_vscodium.scala	Fri Jan 17 23:00:13 2025 +0000
@@ -81,12 +81,7 @@
 
     def get_vscodium_repository(build_dir: Path, progress: Progress = new Progress): Unit = {
       progress.echo("Getting VSCodium repository ...")
-      Isabelle_System.bash(
-        List(
-          "set -e",
-          "git clone -n " + Bash.string(vscodium_repository) + " .",
-          "git checkout -q " + Bash.string(version)
-        ).mkString("\n"), cwd = build_dir).check
+      Isabelle_System.git_clone(vscodium_repository, build_dir, checkout = version)
 
       progress.echo("Getting VSCode repository ...")
       Isabelle_System.bash(environment + "\n" + "./get_repo.sh", cwd = build_dir).check
@@ -286,13 +281,13 @@
       progress.echo("Prepare ...")
       Isabelle_System.with_copy_dir(vscode_dir, vscode_dir.orig) {
         progress.bash(
-          List(
+          Library.make_lines(
             "set -e",
             platform_info.environment,
             "./prepare_vscode.sh",
             // enforce binary diff of code.xpm
             "cp vscode/resources/linux/code.png vscode/resources/linux/rpm/code.xpm"
-          ).mkString("\n"), cwd = build_dir, echo = progress.verbose).check
+          ), cwd = build_dir, echo = progress.verbose).check
         Isabelle_System.make_patch(build_dir, vscode_dir.orig.base, vscode_dir.base,
           diff_options = "--exclude=.git --exclude=node_modules")
       }
diff -r 1c003b308c98 -r e4ff4a4ee4ec src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Jan 17 20:24:09 2025 +0000
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Jan 17 23:00:13 2025 +0000
@@ -45,6 +45,8 @@
         .replace('\t',' ')
 
     lazy val gui_text: String = Library.string_builder(line_range.length * 2) { s =>
+      val style = GUI.Style_HTML
+
       // see also HyperSearchResults.highlightString
       s ++= "<html><b>"
       s ++= line.toString
@@ -58,15 +60,15 @@
       var last = plain_start
       for (range <- JEdit_Lib.search_text(buffer, search_range, regex)) {
         val next = range.start - line_start
-        if (last < next) s ++= line_text.substring(last, next)
+        if (last < next) s ++= style.make_text(line_text.substring(last, next))
         s ++= "<span style=\""
         s ++= highlight_style
         s ++= "\">"
-        s ++= line_text.substring(next, next + range.length)
+        s ++= style.make_text(line_text.substring(next, next + range.length))
         s ++= "</span>"
         last = range.stop - line_start
       }
-      if (last < plain_stop) s ++= line_text.substring(last)
+      if (last < plain_stop) s ++= style.make_text(line_text.substring(last))
       s ++= "</html>"
     }
     override def toString: String = gui_text