# HG changeset patch
# User wenzelm
# Date 1737414091 -3600
# Node ID 372ff330a9d95d22dbe4ba8458084d4492a55cd7
# Parent  67ea7246a9d0841c3d51f8b8de1811b4dc63e973
tuned names, following HOL Light sources;

diff -r 67ea7246a9d0 -r 372ff330a9d9 src/HOL/Import/import_rule.ML
--- 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