Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
minor performance tuning;
authorwenzelm
Mon, 08 Jan 2024 21:53:16 +0100
changeset 79436 253d86888e84
parent 79435 e83f5e3813b1
child 79437 848073637388
minor performance tuning;
src/Pure/more_thm.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/more_thm.ML	Mon Jan 08 21:46:43 2024 +0100
+++ b/src/Pure/more_thm.ML	Mon Jan 08 21:53:16 2024 +0100
@@ -533,7 +533,9 @@
       map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S))))
         tfrees' tfrees;
     val strip = map (apply2 TFree) (tfrees ~~ tfrees');
-    val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t;
+    val t' =
+      (Term.map_types o Term.map_atyps_same)
+        (Same.function_eq (op =) (perhaps (AList.lookup (op =) strip))) t;
   in (strip, recover, t') end;
 
 fun add_axiom ctxt (b, prop) thy =
isabelle