# HG changeset patch
# User wenzelm
# Date 1630920738 -7200
# Node ID eb265f54e3ce32356dd1e555bba3364448e8e0b9
# Parent  36774e8af3db272b9e0fead3633a632e1cfd9a10
more efficient operations: traverse hyps only when required;

diff -r 36774e8af3db -r eb265f54e3ce src/HOL/Eisbach/eisbach_rule_insts.ML
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Sun Sep 05 23:21:32 2021 +0200
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Mon Sep 06 11:32:18 2021 +0200
@@ -26,10 +26,10 @@
 
 fun add_thm_insts ctxt thm =
   let
-    val tyvars = Thm.fold_terms Term.add_tvars thm [];
+    val tyvars = Thm.fold_terms {hyps = false} Term.add_tvars thm [];
     val tyvars' = tyvars |> map (mk_term_type_internal o TVar);
 
-    val tvars = Thm.fold_terms Term.add_vars thm [];
+    val tvars = Thm.fold_terms {hyps = false} Term.add_vars thm [];
     val tvars' = tvars  |> map (Logic.mk_term o Var);
 
     val conj =
@@ -56,8 +56,8 @@
 
 fun instantiate_xis ctxt insts thm =
   let
-    val tyvars = Thm.fold_terms Term.add_tvars thm [];
-    val tvars = Thm.fold_terms Term.add_vars thm [];
+    val tyvars = Thm.fold_terms {hyps = false} Term.add_tvars thm [];
+    val tvars = Thm.fold_terms {hyps = false} Term.add_vars thm [];
 
     fun add_inst (xi, t) (Ts, ts) =
       (case AList.lookup (op =) tyvars xi of
diff -r 36774e8af3db -r eb265f54e3ce src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Sun Sep 05 23:21:32 2021 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Mon Sep 06 11:32:18 2021 +0200
@@ -131,7 +131,7 @@
       ||> Sign.restore_naming thy;
 
     val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []);
-    val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
+    val rvs = rev (Thm.fold_terms {hyps = false} Term.add_vars thm' []);
     val ivs1 = map Var (filter_out (fn (_, T) => \<^type_name>\<open>bool\<close> = tname_of (body_type T)) ivs);
     val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
 
diff -r 36774e8af3db -r eb265f54e3ce src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Sep 05 23:21:32 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML	Mon Sep 06 11:32:18 2021 +0200
@@ -307,8 +307,8 @@
     val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms;
 
     (*export fixes*)
-    val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
-    val frees = map Free (Thm.fold_terms Term.add_frees th' []);
+    val tfrees = map TFree (Thm.fold_terms {hyps = true} Term.add_tfrees th' []);
+    val frees = map Free (Thm.fold_terms {hyps = true} Term.add_frees th' []);
     val (th'' :: vs) =
       (th' :: map (Drule.mk_term o Thm.cterm_of ctxt) (map Logic.mk_type tfrees @ frees))
       |> Variable.export ctxt thy_ctxt
diff -r 36774e8af3db -r eb265f54e3ce src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Sun Sep 05 23:21:32 2021 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Mon Sep 06 11:32:18 2021 +0200
@@ -115,8 +115,8 @@
     val (type_insts, term_insts) =
       List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) raw_insts;
 
-    val tvars = Term_Subst.TVars.build (Thm.fold_terms Term_Subst.add_tvars thm);
-    val vars = Term_Subst.Vars.build (Thm.fold_terms Term_Subst.add_vars thm);
+    val tvars = Term_Subst.TVars.build (Thm.fold_terms {hyps = false} Term_Subst.add_tvars thm);
+    val vars = Term_Subst.Vars.build (Thm.fold_terms {hyps = false} Term_Subst.add_vars thm);
 
     (*eigen-context*)
     val (_, ctxt1) = ctxt
diff -r 36774e8af3db -r eb265f54e3ce src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun Sep 05 23:21:32 2021 +0200
+++ b/src/Pure/drule.ML	Mon Sep 06 11:32:18 2021 +0200
@@ -184,7 +184,7 @@
       |> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T));
     val Ts = map Term.fastype_of ps;
     val inst =
-      Term_Subst.Vars.build (th |> (Thm.fold_terms o Term.fold_aterms)
+      Term_Subst.Vars.build (th |> (Thm.fold_terms {hyps = false} o Term.fold_aterms)
         (fn t => fn inst =>
           (case t of
             Var (xi, T) =>
diff -r 36774e8af3db -r eb265f54e3ce src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Sep 05 23:21:32 2021 +0200
+++ b/src/Pure/more_thm.ML	Mon Sep 06 11:32:18 2021 +0200
@@ -138,12 +138,15 @@
 val eq_ctyp = op = o apply2 Thm.typ_of;
 val op aconvc = op aconv o apply2 Thm.term_of;
 
-val add_tvars = Thm.fold_atomic_ctyps (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a);
-val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a);
-val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a);
+val add_tvars =
+  Thm.fold_atomic_ctyps {hyps = false} (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a);
+val add_vars =
+  Thm.fold_atomic_cterms {hyps = false} (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a);
+val add_frees =
+  Thm.fold_atomic_cterms {hyps = true} (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a);
 
 fun frees_of th =
-  (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms
+  (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true}
     (fn a => fn (set, list) =>
       (case Thm.term_of a of
         Free v =>
@@ -390,7 +393,7 @@
 fun forall_elim_vars_list vars i th =
   let
     val used =
-      (Thm.fold_terms o Term.fold_aterms)
+      (Thm.fold_terms {hyps = false} o Term.fold_aterms)
         (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I) th [];
     val vars' = (Name.variant_list used (map #1 vars), vars)
       |> ListPair.map (fn (x, (_, T)) => Thm.var ((x, i), T));
@@ -449,11 +452,10 @@
       zip_options xs ys handle ListPair.UnequalLengths =>
         err "more instantiations than variables in thm";
 
-    val thm' =
-      Thm.instantiate ((zip_vars (build_rev (Thm.fold_terms Term.add_tvars thm)) cTs), []) thm;
-    val thm'' =
-      Thm.instantiate ([], zip_vars (build_rev (Thm.fold_terms Term.add_vars thm')) cts) thm';
-  in thm'' end;
+    val instT = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_tvars thm)) cTs;
+    val thm' = Thm.instantiate (instT, []) thm;
+    val inst = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_vars thm')) cts;
+  in Thm.instantiate ([], inst) thm' end;
 
 
 (* forall_intr_frees: generalization over all suitable Free variables *)
@@ -465,7 +467,7 @@
        (fold Term_Subst.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #>
         fold Term_Subst.add_frees (Thm.hyps_of th));
     val (_, frees) =
-      (th, (fixed0, [])) |-> Thm.fold_atomic_cterms (fn a => fn (fixed, frees) =>
+      (th, (fixed0, [])) |-> Thm.fold_atomic_cterms {hyps = false} (fn a => fn (fixed, frees) =>
         (case Thm.term_of a of
           Free v =>
             if not (Term_Subst.Frees.defined fixed v)
diff -r 36774e8af3db -r eb265f54e3ce src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Sep 05 23:21:32 2021 +0200
+++ b/src/Pure/thm.ML	Mon Sep 06 11:32:18 2021 +0200
@@ -59,9 +59,9 @@
   val first_order_match: cterm * cterm ->
     ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   (*theorems*)
-  val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
-  val fold_atomic_ctyps: (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a
-  val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
+  val fold_terms: {hyps: bool} -> (term -> 'a -> 'a) -> thm -> 'a -> 'a
+  val fold_atomic_ctyps: {hyps: bool} -> (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a
+  val fold_atomic_cterms: {hyps: bool} -> (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
   val terms_of_tpairs: (term * term) list -> term list
   val full_prop_of: thm -> term
   val theory_id: thm -> Context.theory_id
@@ -434,16 +434,16 @@
 
 fun rep_thm (Thm (_, args)) = args;
 
-fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) =
-  fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps;
+fun fold_terms h f (Thm (_, {tpairs, prop, hyps, ...})) =
+  fold (fn (t, u) => f t #> f u) tpairs #> f prop #> #hyps h ? fold f hyps;
 
-fun fold_atomic_ctyps f (th as Thm (_, {cert, maxidx, shyps, ...})) =
+fun fold_atomic_ctyps h f (th as Thm (_, {cert, maxidx, shyps, ...})) =
   let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps}
-  in (fold_terms o fold_types o fold_atyps) (f o ctyp) th end;
+  in (fold_terms h o fold_types o fold_atyps) (f o ctyp) th end;
 
-fun fold_atomic_cterms f (th as Thm (_, {cert, maxidx, shyps, ...})) =
+fun fold_atomic_cterms h f (th as Thm (_, {cert, maxidx, shyps, ...})) =
   let fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps} in
-    (fold_terms o fold_aterms)
+    (fold_terms h o fold_aterms)
       (fn t as Const (_, T) => f (cterm t T)
         | t as Free (_, T) => f (cterm t T)
         | t as Var (_, T) => f (cterm t T)
@@ -985,7 +985,7 @@
 
 (*Dangling sort constraints of a thm*)
 fun extra_shyps (th as Thm (_, {shyps, ...})) =
-  Sorts.subtract (fold_terms Sorts.insert_term th []) shyps;
+  Sorts.subtract (fold_terms {hyps = true} Sorts.insert_term th []) shyps;
 
 (*Remove extra sorts that are witnessed by type signature information*)
 fun strip_shyps thm =
@@ -1001,7 +1001,8 @@
         fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1));
         fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)];
 
-        val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
+        val present =
+          (fold_terms {hyps = true} o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
         val extra = fold (Sorts.remove_sort o #2) present shyps;
         val witnessed = Sign.witness_sorts thy present extra;
         val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize);
diff -r 36774e8af3db -r eb265f54e3ce src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sun Sep 05 23:21:32 2021 +0200
+++ b/src/Pure/variable.ML	Mon Sep 06 11:32:18 2021 +0200
@@ -267,7 +267,7 @@
 val declare_prf =
   Proofterm.fold_proof_terms_types declare_internal (declare_internal o Logic.mk_type);
 
-val declare_thm = Thm.fold_terms declare_internal;
+val declare_thm = Thm.fold_terms {hyps = true} declare_internal;
 
 
 (* renaming term/type frees *)
@@ -689,7 +689,9 @@
   in ((xs ~~ ps', goal'), ctxt') end;
 
 fun focus_subgoal bindings i st =
-  let val all_vars = Term_Subst.Vars.build (Thm.fold_terms Term_Subst.add_vars st) in
+  let
+    val all_vars = Term_Subst.Vars.build (Thm.fold_terms {hyps = false} Term_Subst.add_vars st);
+  in
     Term_Subst.Vars.fold (unbind_term o #1 o #1) all_vars #>
     Term_Subst.Vars.fold (declare_constraints o Var o #1) all_vars #>
     focus_cterm bindings (Thm.cprem_of st i)
diff -r 36774e8af3db -r eb265f54e3ce src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Sun Sep 05 23:21:32 2021 +0200
+++ b/src/Tools/misc_legacy.ML	Mon Sep 06 11:32:18 2021 +0200
@@ -235,7 +235,7 @@
 fun freeze_thaw_robust ctxt th =
  let val fth = Thm.legacy_freezeT th
  in
-   case Thm.fold_terms Term.add_vars fth [] of
+   case Thm.fold_terms {hyps = false} Term.add_vars fth [] of
        [] => (fth, fn _ => fn x => x)   (*No vars: nothing to do!*)
      | vars =>
          let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))