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.
tuned;
authorwenzelm
Sat, 16 Oct 2021 21:14:24 +0200
changeset 74534 638301b86f0a
parent 74533 5cab031e2344
child 74535 2f8e8dc9b522
tuned;
src/HOL/Tools/Function/function_core.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Function/function_core.ML	Sat Oct 16 20:32:25 2021 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sat Oct 16 21:14:24 2021 +0200
@@ -622,8 +622,8 @@
         local open Conv in
           val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
           val sih =
-            fconv_rule (Conv.binder_conv
-              (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt1) aihyp
+            fconv_rule
+              (binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt1) aihyp
         end
 
         fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
isabelle