tuned messages;
authorwenzelm
Tue Jun 04 17:04:18 2019 +0200 (6 weeks ago)
changeset 7032265b880d4efbb
parent 70321 24877d539fb8
child 70323 2943934a169d
tuned messages;
src/HOL/Tools/Lifting/lifting_info.ML
src/HOL/Tools/Lifting/lifting_setup.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Tue Jun 04 16:47:05 2019 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Tue Jun 04 17:04:18 2019 +0200
     1.3 @@ -248,14 +248,13 @@
     1.4    let
     1.5      fun prt_quot (qty_name, {quot_thm, pcr_info}: quotient) =
     1.6        Pretty.block (separate (Pretty.brk 2)
     1.7 -       [Pretty.str "type:",
     1.8 -        Pretty.str qty_name,
     1.9 -        Pretty.str "quot. thm:",
    1.10 -        Syntax.pretty_term ctxt (Thm.prop_of quot_thm),
    1.11 -        Pretty.str "pcrel_def thm:",
    1.12 -        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o Thm.prop_of o #pcrel_def) pcr_info,
    1.13 -        Pretty.str "pcr_cr_eq thm:",
    1.14 -        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o Thm.prop_of o #pcr_cr_eq) pcr_info])
    1.15 +        ([Pretty.str "type:", Pretty.str qty_name,
    1.16 +          Pretty.str "quot thm:", Thm.pretty_thm ctxt quot_thm] @
    1.17 +         (case pcr_info of
    1.18 +           NONE => []
    1.19 +         | SOME {pcrel_def, pcr_cr_eq, ...} =>
    1.20 +            [Pretty.str "pcrel_def thm:", Thm.pretty_thm ctxt pcrel_def,
    1.21 +             Pretty.str "pcr_cr_eq thm:", Thm.pretty_thm ctxt pcr_cr_eq])))
    1.22    in
    1.23      map prt_quot (Symtab.dest (get_quotients ctxt))
    1.24      |> Pretty.big_list "quotients:"
     2.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Jun 04 16:47:05 2019 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Jun 04 17:04:18 2019 +0200
     2.3 @@ -562,12 +562,13 @@
     2.4        end
     2.5  
     2.6      fun generate_parametric_rel_eq ctxt transfer_rule opt_param_thm =
     2.7 -      option_fold transfer_rule
     2.8 -        (Lifting_Def.generate_parametric_transfer_rule ctxt transfer_rule) opt_param_thm
     2.9 -      handle Lifting_Term.MERGE_TRANSFER_REL msg =>
    2.10 -        error (cat_lines
    2.11 -          ["Generation of a parametric transfer rule for the quotient relation failed.",
    2.12 -          (Pretty.string_of (Pretty.block [Pretty.str "Reason:", Pretty.brk 2, msg]))])
    2.13 +      (case opt_param_thm of
    2.14 +        NONE => transfer_rule
    2.15 +      | SOME param_thm =>
    2.16 +          (Lifting_Def.generate_parametric_transfer_rule ctxt transfer_rule param_thm
    2.17 +            handle Lifting_Term.MERGE_TRANSFER_REL msg =>
    2.18 +              error ("Generation of a parametric transfer rule for the quotient relation failed:\n"
    2.19 +                ^ Pretty.string_of msg)))
    2.20  
    2.21      fun setup_transfer_rules_par ctxt notes =
    2.22        let