--- a/src/HOL/Tools/Lifting/lifting_info.ML Tue Jun 04 16:47:05 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Tue Jun 04 17:04:18 2019 +0200
@@ -248,14 +248,13 @@
let
fun prt_quot (qty_name, {quot_thm, pcr_info}: quotient) =
Pretty.block (separate (Pretty.brk 2)
- [Pretty.str "type:",
- Pretty.str qty_name,
- Pretty.str "quot. thm:",
- Syntax.pretty_term ctxt (Thm.prop_of quot_thm),
- Pretty.str "pcrel_def thm:",
- option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o Thm.prop_of o #pcrel_def) pcr_info,
- Pretty.str "pcr_cr_eq thm:",
- option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o Thm.prop_of o #pcr_cr_eq) pcr_info])
+ ([Pretty.str "type:", Pretty.str qty_name,
+ Pretty.str "quot thm:", Thm.pretty_thm ctxt quot_thm] @
+ (case pcr_info of
+ NONE => []
+ | SOME {pcrel_def, pcr_cr_eq, ...} =>
+ [Pretty.str "pcrel_def thm:", Thm.pretty_thm ctxt pcrel_def,
+ Pretty.str "pcr_cr_eq thm:", Thm.pretty_thm ctxt pcr_cr_eq])))
in
map prt_quot (Symtab.dest (get_quotients ctxt))
|> Pretty.big_list "quotients:"
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Jun 04 16:47:05 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Jun 04 17:04:18 2019 +0200
@@ -562,12 +562,13 @@
end
fun generate_parametric_rel_eq ctxt transfer_rule opt_param_thm =
- option_fold transfer_rule
- (Lifting_Def.generate_parametric_transfer_rule ctxt transfer_rule) opt_param_thm
- handle Lifting_Term.MERGE_TRANSFER_REL msg =>
- error (cat_lines
- ["Generation of a parametric transfer rule for the quotient relation failed.",
- (Pretty.string_of (Pretty.block [Pretty.str "Reason:", Pretty.brk 2, msg]))])
+ (case opt_param_thm of
+ NONE => transfer_rule
+ | SOME param_thm =>
+ (Lifting_Def.generate_parametric_transfer_rule ctxt transfer_rule param_thm
+ handle Lifting_Term.MERGE_TRANSFER_REL msg =>
+ error ("Generation of a parametric transfer rule for the quotient relation failed:\n"
+ ^ Pretty.string_of msg)))
fun setup_transfer_rules_par ctxt notes =
let