tuned;
authorwenzelm
Mon Jun 03 23:29:05 2019 +0200 (6 weeks ago)
changeset 7031256f96489478c
parent 70311 e49bf4ebf330
child 70313 9c19e15c8548
tuned;
src/HOL/Tools/Function/function_common.ML
     1.1 --- a/src/HOL/Tools/Function/function_common.ML	Mon Jun 03 21:47:54 2019 +0200
     1.2 +++ b/src/HOL/Tools/Function/function_common.ML	Mon Jun 03 23:29:05 2019 +0200
     1.3 @@ -114,7 +114,7 @@
     1.4          inducts = Option.map fact inducts, termination = thm termination,
     1.5          totality = Option.map thm totality, defname = Morphism.binding phi defname,
     1.6          is_partial = is_partial, cases = fact cases,
     1.7 -        elims = Option.map (map fact) elims, pelims = map fact pelims }
     1.8 +        pelims = map fact pelims, elims = Option.map (map fact) elims }
     1.9      end
    1.10  
    1.11