# HG changeset patch
# User wenzelm
# Date 1630923077 -7200
# Node ID 12dac3698efdbc5b0f01f1f694dd2b81a91402c2
# Parent  de383840425f10957dfe2e47fe8138d205643e1c
clarified signature;
minor performance tuning;

diff -r de383840425f -r 12dac3698efd src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Sep 06 11:55:54 2021 +0200
+++ b/src/Pure/drule.ML	Mon Sep 06 12:11:17 2021 +0200
@@ -166,10 +166,7 @@
 
 (*Generalization over Vars -- canonical order*)
 fun forall_intr_vars th =
-  let
-    val vs =
-      build (th |> Thm.fold_atomic_cterms {hyps = false} (fn a =>
-        is_Var (Thm.term_of a) ? insert (op aconvc) a));
+  let val vs = build (th |> Thm.fold_atomic_cterms {hyps = false} Term.is_Var (insert (op aconvc)))
   in fold Thm.forall_intr vs th end;
 
 fun outer_params t =
diff -r de383840425f -r 12dac3698efd src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Sep 06 11:55:54 2021 +0200
+++ b/src/Pure/more_thm.ML	Mon Sep 06 12:11:17 2021 +0200
@@ -138,32 +138,23 @@
 val op aconvc = op aconv o apply2 Thm.term_of;
 
 val add_tvars =
-  Thm.fold_atomic_ctyps {hyps = false} (fn cT => fn tab =>
-    (case Thm.typ_of cT of
-      TVar v =>
-        if not (Term_Subst.TVars.defined tab v)
-        then Term_Subst.TVars.update (v, cT) tab
-        else tab
-    | _ => tab));
+  Thm.fold_atomic_ctyps {hyps = false} Term.is_TVar (fn cT => fn tab =>
+    let val v = Term.dest_TVar (Thm.typ_of cT)
+    in tab |> not (Term_Subst.TVars.defined tab v) ? Term_Subst.TVars.update (v, cT) end);
 
 val add_vars =
-  Thm.fold_atomic_cterms {hyps = false} (fn ct => fn tab =>
-    (case Thm.term_of ct of
-      Var v =>
-        if not (Term_Subst.Vars.defined tab v)
-        then Term_Subst.Vars.update (v, ct) tab
-        else tab
-    | _ => tab));
+  Thm.fold_atomic_cterms {hyps = false} Term.is_Var (fn ct => fn tab =>
+    let val v = Term.dest_Var (Thm.term_of ct)
+    in tab |> not (Term_Subst.Vars.defined tab v) ? Term_Subst.Vars.update (v, ct) end);
 
 fun frees_of th =
-  (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true}
-    (fn a => fn (set, list) =>
-      (case Thm.term_of a of
-        Free v =>
-          if not (Term_Subst.Frees.defined set v)
-          then (Term_Subst.Frees.add (v, ()) set, a :: list)
-          else (set, list)
-      | _ => (set, list)))
+  (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true} Term.is_Free
+    (fn ct => fn (set, list) =>
+      let val v = Term.dest_Free (Thm.term_of ct) in
+        if not (Term_Subst.Frees.defined set v)
+        then (Term_Subst.Frees.add (v, ()) set, ct :: list)
+        else (set, list)
+      end)
   |> #2;
 
 
@@ -477,13 +468,13 @@
        (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 {hyps = false} (fn a => fn (fixed, frees) =>
-        (case Thm.term_of a of
-          Free v =>
+      (th, (fixed0, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Free
+        (fn ct => fn (fixed, frees) =>
+          let val v = Term.dest_Free (Thm.term_of ct) in
             if not (Term_Subst.Frees.defined fixed v)
-            then (Term_Subst.Frees.add (v, ()) fixed, a :: frees)
+            then (Term_Subst.Frees.add (v, ()) fixed, ct :: frees)
             else (fixed, frees)
-        | _ => (fixed, frees)));
+          end);
   in fold Thm.forall_intr frees th end;
 
 
diff -r de383840425f -r 12dac3698efd src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Sep 06 11:55:54 2021 +0200
+++ b/src/Pure/thm.ML	Mon Sep 06 12:11:17 2021 +0200
@@ -60,8 +60,8 @@
     ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   (*theorems*)
   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 fold_atomic_ctyps: {hyps: bool} -> (typ -> bool) -> (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a
+  val fold_atomic_cterms: {hyps: bool} -> (term -> 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
@@ -437,16 +437,19 @@
 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 h f (th as Thm (_, {cert, maxidx, shyps, ...})) =
+fun fold_atomic_ctyps h g f (th as Thm (_, {cert, maxidx, shyps, ...})) =
   let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps}
-  in (fold_terms h o fold_types o fold_atyps) (f o ctyp) th end;
+  in (fold_terms h o fold_types o fold_atyps) (fn T => if g T then f (ctyp T) else I) th end;
 
-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
+fun fold_atomic_cterms h g f (th as Thm (_, {cert, maxidx, shyps, ...})) =
+  let
+    fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps};
+    fun apply t T = if g t then f (cterm t T) else I;
+  in
     (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)
+      (fn t as Const (_, T) => apply t T
+        | t as Free (_, T) => apply t T
+        | t as Var (_, T) => apply t T
         | _ => I) th
   end;