equal
deleted
inserted
replaced
1280 let |
1280 let |
1281 val subtrm = REGULARIZE_trm lthy t t' |
1281 val subtrm = REGULARIZE_trm lthy t t' |
1282 in |
1282 in |
1283 if ty = ty' |
1283 if ty = ty' |
1284 then Abs (x, ty, subtrm) |
1284 then Abs (x, ty, subtrm) |
1285 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
1285 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
1286 end |
1286 end |
1287 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
1287 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
1288 let |
1288 let |
1289 val subtrm = apply_subt (REGULARIZE_trm lthy) t t' |
1289 val subtrm = apply_subt (REGULARIZE_trm lthy) t t' |
1290 in |
1290 in |
1390 |
1390 |
1391 fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))] |
1391 fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))] |
1392 *} |
1392 *} |
1393 |
1393 |
1394 ML {* |
1394 ML {* |
|
1395 (* FIXME: change rel_refl rel_eqv *) |
1395 fun REGULARIZE_tac' lthy rel_refl rel_eqv = |
1396 fun REGULARIZE_tac' lthy rel_refl rel_eqv = |
1396 (REPEAT1 o FIRST1) |
1397 (REPEAT1 o FIRST1) |
1397 [(K (print_tac "start")) THEN' (K no_tac), |
1398 [(K (print_tac "start")) THEN' (K no_tac), |
1398 DT lthy "1" (rtac rel_refl), |
1399 DT lthy "1" (rtac rel_refl), |
1399 DT lthy "2" atac, |
1400 DT lthy "2" atac, |