411 in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) refl] end; |
411 in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) refl] end; |
412 val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs |
412 val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs |
413 val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco; |
413 val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco; |
414 val ctxt = ProofContext.init thy; |
414 val ctxt = ProofContext.init thy; |
415 val simpset = Simplifier.context ctxt |
415 val simpset = Simplifier.context ctxt |
416 (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]); |
416 (Simplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]); |
417 val cos = map (fn (co, tys) => |
417 val cos = map (fn (co, tys) => |
418 (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs; |
418 (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs; |
419 val tac = ALLGOALS (simp_tac simpset) |
419 val tac = ALLGOALS (simp_tac simpset) |
420 THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]); |
420 THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]); |
421 val distinct = |
421 val distinct = |