Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/Code/code_preproc.ML
changeset 75353 05f7f5454cb6
parent 74561 8e6c973003c8 
--- a/src/Tools/Code/code_preproc.ML	Sun Mar 27 19:27:50 2022 +0000
+++ b/src/Tools/Code/code_preproc.ML	Sun Mar 27 19:27:52 2022 +0000
@@ -201,7 +201,7 @@
   let
     val t = Thm.term_of ct;
     val vs_original =
-      fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t [];
+      build (fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t);
     val vs_normalized = Name.invent_names Name.context Name.aT (map snd vs_original);
     val normalize =
       map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized));
isabelle