src/HOL/Tools/Function/function_common.ML
changeset 70312 56f96489478c
parent 67664 ad2b3e330c27
child 70326 aa7c49651f4e
     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