--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sat Oct 29 00:39:32 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sat Oct 29 00:39:33 2016 +0200
@@ -785,7 +785,7 @@
fun prove_split selss goal =
Variable.add_free_names lthy goal []
|> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
- mk_split_tac ctxt ms uexhaust_thm case_thms selss inject_thmss distinct_thmsss))
+ mk_split_tac ctxt uexhaust_thm case_thms selss inject_thmss distinct_thmsss))
|> Thm.close_derivation;
fun prove_split_asm asm_goal split_thm =
@@ -805,13 +805,12 @@
(thm, asm_thm)
end;
- val (sel_defs, all_sel_thms, sel_thmss, disc_defs, nontriv_disc_defs, disc_thmss,
- nontriv_disc_thmss, discI_thms, nontriv_discI_thms, distinct_disc_thms,
- distinct_disc_thmsss, exhaust_disc_thms, exhaust_sel_thms, all_collapse_thms,
- safe_collapse_thms, expand_thms, split_sel_thms, split_sel_asm_thms, case_eq_if_thms,
- disc_eq_case_thms) =
+ val (sel_defs, all_sel_thms, sel_thmss, nontriv_disc_defs, disc_thmss, nontriv_disc_thmss,
+ discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss,
+ exhaust_disc_thms, exhaust_sel_thms, all_collapse_thms, safe_collapse_thms,
+ expand_thms, split_sel_thms, split_sel_asm_thms, case_eq_if_thms, disc_eq_case_thms) =
if no_discs_sels then
- ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
+ ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
else
let
val udiscs = map (rapp u) discs;
@@ -1049,11 +1048,11 @@
|> Conjunction.elim_balanced (length goals)
end;
in
- (sel_defs, all_sel_thms, sel_thmss, disc_defs, nontriv_disc_defs, disc_thmss,
- nontriv_disc_thmss, discI_thms, nontriv_discI_thms, distinct_disc_thms,
- distinct_disc_thmsss, [exhaust_disc_thm], [exhaust_sel_thm], all_collapse_thms,
- safe_collapse_thms, [expand_thm], [split_sel_thm], [split_sel_asm_thm],
- [case_eq_if_thm], disc_eq_case_thms)
+ (sel_defs, all_sel_thms, sel_thmss, nontriv_disc_defs, disc_thmss, nontriv_disc_thmss,
+ discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss,
+ [exhaust_disc_thm], [exhaust_sel_thm], all_collapse_thms, safe_collapse_thms,
+ [expand_thm], [split_sel_thm], [split_sel_asm_thm], [case_eq_if_thm],
+ disc_eq_case_thms)
end;
val case_distrib_thm =
@@ -1113,8 +1112,7 @@
|> map (fn (thmN, thms, attrs) =>
((qualify true (Binding.name thmN), attrs), [(thms, [])]));
- val (noted, lthy') =
- lthy
+ val (noted, lthy') = lthy
|> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms)
|> fold (Spec_Rules.add Spec_Rules.Equational)
(AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms))
@@ -1123,14 +1121,15 @@
|> Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Case_Translation.register
(Morphism.term phi casex) (map (Morphism.term phi) ctrs))
- |> Local_Theory.background_theory (fold (fold Code.del_eqn) [nontriv_disc_defs, sel_defs])
+ |> Local_Theory.background_theory
+ (fold (fold Code.del_eqn_silent) [nontriv_disc_defs, sel_defs])
|> plugins code_plugin ?
- Local_Theory.declaration {syntax = false, pervasive = false}
- (fn phi => Context.mapping
- (add_ctr_code fcT_name (map (Morphism.typ phi) As)
- (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
- (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
- I)
+ Local_Theory.declaration {syntax = false, pervasive = false}
+ (fn phi => Context.mapping
+ (add_ctr_code fcT_name (map (Morphism.typ phi) As)
+ (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
+ (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
+ I)
|> Local_Theory.notes (anonymous_notes @ notes)
(* for "datatype_realizer.ML": *)
|>> name_noted_thms fcT_name exhaustN;
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Oct 29 00:39:32 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Oct 29 00:39:33 2016 +0200
@@ -406,25 +406,27 @@
handle Sorts.CLASS_ERROR _ => NONE
fun ensure_sort (((sort_vs, aux_sort), sort), (the_descr, instantiate)) config raw_tycos thy =
- let
- val algebra = Sign.classes_of thy
- val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = the_descr thy raw_tycos
- val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs
- fun insts_of sort constr = (map (rpair sort) o flat o maps snd o maps snd)
- (Old_Datatype_Aux.interpret_construction descr vs constr)
- val insts = insts_of sort { atyp = single, dtyp = (K o K o K) [] }
- @ insts_of aux_sort { atyp = K [], dtyp = K o K }
- val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos
- in
- if has_inst then thy
- else
- (case perhaps_constrain thy insts vs of
- SOME constrain =>
- instantiate config descr
- (map constrain vs) tycos prfx (names, auxnames)
- ((apply2 o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
- | NONE => thy)
- end
+ (case try (the_descr thy) raw_tycos of
+ NONE => thy
+ | SOME (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =>
+ let
+ val algebra = Sign.classes_of thy
+ val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs
+ fun insts_of sort constr = (map (rpair sort) o flat o maps snd o maps snd)
+ (Old_Datatype_Aux.interpret_construction descr vs constr)
+ val insts = insts_of sort { atyp = single, dtyp = (K o K o K) [] }
+ @ insts_of aux_sort { atyp = K [], dtyp = K o K }
+ val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos
+ in
+ if has_inst then thy
+ else
+ (case perhaps_constrain thy insts vs of
+ SOME constrain =>
+ instantiate config descr
+ (map constrain vs) tycos prfx (names, auxnames)
+ ((apply2 o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
+ | NONE => thy)
+ end)
fun ensure_common_sort_datatype (sort, instantiate) =
ensure_sort (((@{sort typerep}, @{sort term_of}), sort),