src/HOL/Tools/Function/function_common.ML

         fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
         pinducts = fact pinducts, simps = Option.map fact simps,
         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
 
 
 (* profiling *)