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.
more uniform Type_Infer_Context.infer_types_finished, despite subtle differences of Type_Infer.fixate vs. Proof_Context.standard_term_check_finish;
authorwenzelm
Wed, 07 Aug 2024 20:15:03 +0200
changeset 80669 e8a47adda46b
parent 80668 863b6699274e
child 80670 cbfc1058df7c
more uniform Type_Infer_Context.infer_types_finished, despite subtle differences of Type_Infer.fixate vs. Proof_Context.standard_term_check_finish;
src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed Aug 07 20:11:05 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed Aug 07 20:15:03 2024 +0200
@@ -1028,8 +1028,7 @@
 
         val deadfixed_T =
           build_map lthy [] [] (mk_undefined o op -->) (apply2 tupleT_of_funT (param1_T, param2_T))
-          |> singleton (Type_Infer_Context.infer_types lthy)
-          |> singleton (Type_Infer.fixate lthy false)
+          |> singleton (Type_Infer_Context.infer_types_finished lthy)
           |> type_of
           |> dest_funT
           |-> generalize_types 1
isabelle