equal
deleted
inserted
replaced
854 | (Const (s, ty), Const (s', ty')) => |
854 | (Const (s, ty), Const (s', ty')) => |
855 if s = s' andalso ty = ty' |
855 if s = s' andalso ty = ty' |
856 then rtrm |
856 then rtrm |
857 else rtrm (* FIXME: check correspondence according to definitions *) |
857 else rtrm (* FIXME: check correspondence according to definitions *) |
858 | (rt, qt) => |
858 | (rt, qt) => |
859 let |
|
860 val _ = tracing "default execption" |
|
861 val _ = tracing (PolyML.makestring rt) |
|
862 val _ = tracing (PolyML.makestring qt) |
|
863 in |
|
864 raise (LIFT_MATCH "regularize (default)") |
859 raise (LIFT_MATCH "regularize (default)") |
865 end |
|
866 *} |
860 *} |
867 |
861 |
868 ML {* |
862 ML {* |
869 fun mk_REGULARIZE_goal lthy rtrm qtrm = |
863 fun mk_REGULARIZE_goal lthy rtrm qtrm = |
870 Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm)) |
864 Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm)) |
968 |
962 |
969 |
963 |
970 ML {* |
964 ML {* |
971 (* bound variables need to be treated properly, *) |
965 (* bound variables need to be treated properly, *) |
972 (* as the type of subterms need to be calculated *) |
966 (* as the type of subterms need to be calculated *) |
973 |
|
974 |
967 |
975 fun inj_REPABS lthy (rtrm, qtrm) = |
968 fun inj_REPABS lthy (rtrm, qtrm) = |
976 let |
969 let |
977 val rty = fastype_of rtrm |
970 val rty = fastype_of rtrm |
978 val qty = fastype_of qtrm |
971 val qty = fastype_of qtrm |