# HG changeset patch
# User wenzelm
# Date 1631214845 -7200
# Node ID aed955bb4cb1e40bd42fd7cbc3b52d51d37019c6
# Parent  36f2c4a5c21b52ea2114d93b9ce18c373627ffd5
omit obsolete field "xs": originally from fd0f8fa2b6bd, but later unused;

diff -r 36f2c4a5c21b -r aed955bb4cb1 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Sep 09 17:20:41 2021 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Sep 09 21:14:05 2021 +0200
@@ -572,7 +572,7 @@
 
 val norm_term = Envir.beta_norm oo Term.subst_atomic;
 
-fun bind_def ctxt eq (xs, env, eqs) =
+fun bind_def ctxt eq (env, eqs) =
   let
     val _ = Local_Defs.cert_def ctxt (K []) eq;
     val ((y, T), b) = Local_Defs.abs_def eq;
@@ -580,9 +580,9 @@
     fun err msg = error (msg ^ ": " ^ quote y);
   in
     (case filter (fn (Free (y', _), _) => y = y' | _ => false) env of
-      [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
+      [] => ((Free (y, T), b') :: env, eq :: eqs)
     | dups =>
-        if forall (fn (_, b'') => b' aconv b'') dups then (xs, env, eqs)
+        if forall (fn (_, b'') => b' aconv b'') dups then (env, eqs)
         else err "Attempt to redefine variable")
   end;
 
@@ -604,14 +604,14 @@
 fun eval_text _ _ (Fixes _) text = text
   | eval_text _ _ (Constrains _) text = text
   | eval_text _ is_ext (Assumes asms)
-        (((exts, exts'), (ints, ints')), (xs, env, defs)) =
+        (((exts, exts'), (ints, ints')), (env, defs)) =
       let
         val ts = maps (map #1 o #2) asms;
         val ts' = map (norm_term env) ts;
         val spec' =
           if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
           else ((exts, exts'), (ints @ ts, ints' @ ts'));
-      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
+      in (spec', (env, defs)) end
   | eval_text ctxt _ (Defines defs) (spec, binds) =
       (spec, fold (bind_def ctxt o #1 o #2) defs binds)
   | eval_text _ _ (Notes _) text = text
@@ -639,8 +639,8 @@
 
 fun eval ctxt deps elems =
   let
-    val text' = fold (eval_inst ctxt) deps ((([], []), ([], [])), ([], [], []));
-    val ((spec, (_, _, defs))) = fold (eval_elem ctxt) elems text';
+    val text' = fold (eval_inst ctxt) deps ((([], []), ([], [])), ([], []));
+    val ((spec, (_, defs))) = fold (eval_elem ctxt) elems text';
   in (spec, defs) end;
 
 (* axiomsN: name of theorem set with destruct rules for locale predicates,