changeset 33968 | f94fb13ecbb3 |
parent 33754 | f2957bd46faf |
child 34028 | 1e6206763036 |
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Nov 30 11:42:48 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Nov 30 11:42:49 2009 +0100 @@ -1282,7 +1282,7 @@ val v' = Free (name', T); in lambda v (fst (Datatype.make_case - (ProofContext.init thy) DatatypeCase.Quiet [] v + (ProofContext.init thy) Datatype_Case.Quiet [] v [(HOLogic.mk_tuple out_ts, if null eqs'' then success_t else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $