equal
deleted
inserted
replaced
735 | (Const (s, ty), Const (s', ty')) => |
735 | (Const (s, ty), Const (s', ty')) => |
736 if s = s' andalso ty = ty' |
736 if s = s' andalso ty = ty' |
737 then rtrm |
737 then rtrm |
738 else rtrm (* FIXME: check correspondence according to definitions *) |
738 else rtrm (* FIXME: check correspondence according to definitions *) |
739 | (rt, qt) => |
739 | (rt, qt) => |
740 let |
|
741 val _ = tracing "default execption" |
|
742 val _ = tracing (PolyML.makestring rt) |
|
743 val _ = tracing (PolyML.makestring qt) |
|
744 in |
|
745 raise (LIFT_MATCH "regularize (default)") |
740 raise (LIFT_MATCH "regularize (default)") |
746 end |
|
747 *} |
741 *} |
748 |
742 |
749 ML {* |
743 ML {* |
750 fun mk_REGULARIZE_goal lthy rtrm qtrm = |
744 fun mk_REGULARIZE_goal lthy rtrm qtrm = |
751 Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm)) |
745 Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm)) |
882 |
876 |
883 |
877 |
884 ML {* |
878 ML {* |
885 (* bound variables need to be treated properly, *) |
879 (* bound variables need to be treated properly, *) |
886 (* as the type of subterms need to be calculated *) |
880 (* as the type of subterms need to be calculated *) |
887 |
|
888 |
881 |
889 fun inj_REPABS lthy (rtrm, qtrm) = |
882 fun inj_REPABS lthy (rtrm, qtrm) = |
890 let |
883 let |
891 val rty = fastype_of rtrm |
884 val rty = fastype_of rtrm |
892 val qty = fastype_of qtrm |
885 val qty = fastype_of qtrm |