equal
deleted
inserted
replaced
1113 val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts); |
1113 val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts); |
1114 (* val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) |
1114 (* val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) |
1115 in |
1115 in |
1116 Conv.rewr_conv ti ctrm |
1116 Conv.rewr_conv ti ctrm |
1117 end |
1117 end |
|
1118 (* TODO: We can add a proper error message... *) |
|
1119 handle Bind => Conv.all_conv ctrm |
1118 |
1120 |
1119 *} |
1121 *} |
1120 ML {* |
1122 ML {* |
1121 fun lambda_prs_conv ctxt quot ctrm = |
1123 fun lambda_prs_conv ctxt quot ctrm = |
1122 case (term_of ctrm) of |
1124 case (term_of ctrm) of |