# HG changeset patch
# User wenzelm
# Date 1686053993 -7200
# Node ID 9ccb1ae28f0dc26c5216b08dc9b7942e152c4529
# Parent  e1bd2eb4c407774cfb92a9c677034ef510d710a7
tuned;

diff -r e1bd2eb4c407 -r 9ccb1ae28f0d src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Tue Jun 06 11:33:38 2023 +0200
+++ b/src/Pure/assumption.ML	Tue Jun 06 14:19:53 2023 +0200
@@ -27,10 +27,17 @@
 structure Assumption: ASSUMPTION =
 struct
 
-(** basic rules **)
+(** export operations **)
 
 type export = bool -> cterm list -> (thm -> thm) * (term -> term);
 
+val term_export = fold_rev (fn (e: export, As) => #2 (e false As));
+fun thm_export is_goal = fold_rev (fn (e: export, As) => #1 (e is_goal As));
+
+
+
+(** basic rules **)
+
 (*
     [A]
      :
@@ -132,10 +139,10 @@
 (* export *)
 
 fun export_term inner outer =
-  fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
+  term_export (local_assumptions_of inner outer);
 
 fun export_thm is_goal inner outer =
-  fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer);
+  thm_export is_goal (local_assumptions_of inner outer);
 
 fun export_{goal} inner outer =
   Raw_Simplifier.norm_hhf_protect inner #>