equal
deleted
inserted
replaced
1116 ML {* |
1116 ML {* |
1117 fun lift_error ctxt fun_str rtrm qtrm = |
1117 fun lift_error ctxt fun_str rtrm qtrm = |
1118 let |
1118 let |
1119 val rtrm_str = Syntax.string_of_term ctxt rtrm |
1119 val rtrm_str = Syntax.string_of_term ctxt rtrm |
1120 val qtrm_str = Syntax.string_of_term ctxt qtrm |
1120 val qtrm_str = Syntax.string_of_term ctxt qtrm |
1121 val msg = [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, |
1121 val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, |
1122 "and the lifted theorem", rtrm_str, "do not match"] |
1122 "and the lifted theorem\n", rtrm_str, "do not match"] |
1123 in |
1123 in |
1124 error (space_implode " " msg) |
1124 error (space_implode " " msg) |
1125 end |
1125 end |
1126 *} |
1126 *} |
1127 |
1127 |