src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 51673 4dfa00e264d8
parent 51672 d5c5e088ebdf
child 51689 43a3465805dd
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Jan 22 13:32:41 2013 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Jan 22 14:33:45 2013 +0100
     1.3 @@ -427,7 +427,7 @@
     1.4    end
     1.5  
     1.6  fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
     1.7 -    Datatype_Case.make_case ctxt Datatype_Case.Quiet Name.context (Free (x, T)) (map (fn (t, c) =>
     1.8 +    Case_Translation.make_case ctxt Case_Translation.Quiet Name.context (Free (x, T)) (map (fn (t, c) =>
     1.9        (t, mk_case_term ctxt (p - 1) qs' c)) cs)
    1.10    | mk_case_term ctxt p ((@{const_name All}, _) :: qs') (Universal_Counterexample (t, c)) =
    1.11      if p = 0 then t else mk_case_term ctxt (p - 1) qs' c