# HG changeset patch
# User wenzelm
# Date 1559597345 -7200
# Node ID 56f96489478c887db78b8a5727b4a0ece3f5acdd
# Parent  e49bf4ebf3305211b755c00105f674dbcf090a68
tuned;

diff -r e49bf4ebf330 -r 56f96489478c src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Mon Jun 03 21:47:54 2019 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Mon Jun 03 23:29:05 2019 +0200
@@ -114,7 +114,7 @@
         inducts = Option.map fact inducts, termination = thm termination,
         totality = Option.map thm totality, defname = Morphism.binding phi defname,
         is_partial = is_partial, cases = fact cases,
-        elims = Option.map (map fact) elims, pelims = map fact pelims }
+        pelims = map fact pelims, elims = Option.map (map fact) elims }
     end