# HG changeset patch
# User wenzelm
# Date 1559660658 -7200
# Node ID 65b880d4efbbcc259425793196675a017963dbe8
# Parent  24877d539fb89a4b238801a5f75de1996d403caa
tuned messages;

diff -r 24877d539fb8 -r 65b880d4efbb src/HOL/Tools/Lifting/lifting_info.ML
--- 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:"
diff -r 24877d539fb8 -r 65b880d4efbb src/HOL/Tools/Lifting/lifting_setup.ML
--- 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