src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 43317 f9283eb3a4bf
parent 43314 a9090cabca14
child 43329 84472e198515
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jun 09 08:32:22 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jun 09 09:07:13 2011 +0200
     1.3 @@ -358,8 +358,8 @@
     1.4    end
     1.5  
     1.6  fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
     1.7 -    fst (Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
     1.8 -      (t, mk_case_term ctxt (p - 1) qs' c)) cs))
     1.9 +    Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
    1.10 +      (t, mk_case_term ctxt (p - 1) qs' c)) cs)
    1.11    | mk_case_term ctxt p ((@{const_name All}, (x, T)) :: qs') (Universal_Counterexample (t, c)) =
    1.12      if p = 0 then t else mk_case_term ctxt (p - 1) qs' c
    1.13