equal
deleted
inserted
replaced
1262 let |
1262 let |
1263 val subtrm = REGULARIZE_trm lthy t t' |
1263 val subtrm = REGULARIZE_trm lthy t t' |
1264 in |
1264 in |
1265 if ty = ty' |
1265 if ty = ty' |
1266 then Const (@{const_name "op ="}, ty) $ subtrm |
1266 then Const (@{const_name "op ="}, ty) $ subtrm |
1267 else mk_resp_arg lthy (ty, ty') $ subtrm |
1267 else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm |
1268 end |
1268 end |
1269 | (t1 $ t2, t1' $ t2') => |
1269 | (t1 $ t2, t1' $ t2') => |
1270 (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2') |
1270 (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2') |
1271 | (Free (x, ty), Free (x', ty')) => |
1271 | (Free (x, ty), Free (x', ty')) => |
1272 if x = x' |
1272 if x = x' |