tuned names, following HOL Light sources;

--- a/src/HOL/Import/import_rule.ML	Mon Jan 20 13:03:50 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Tue Jan 21 00:01:31 2025 +0100
@@ -195,18 +195,18 @@
     Thm.instantiate (TVars.empty, inst) th
   end)
 
-fun inst_type lambda =
+fun inst_type theta =
   let
     val tyinst =
-      TFrees.build (lambda |> fold (fn (a, b) =>
+      TFrees.build (theta |> fold (fn (a, b) =>
         TFrees.add (Term.dest_TFree (Thm.typ_of a), b)))
   in
     Thm.instantiate_frees (tyinst, Frees.empty)
   end
 
-fun inst sigma th =
+fun inst theta th =
   let
-    val (dom, rng) = ListPair.unzip (rev sigma)
+    val (dom, rng) = ListPair.unzip (rev theta)
   in
     th |> forall_intr_list dom
        |> forall_elim_list rng