equal
deleted
inserted
replaced
901 in |
901 in |
902 map Thm.varifyT defs_all |
902 map Thm.varifyT defs_all |
903 end |
903 end |
904 *} |
904 *} |
905 |
905 |
906 text {* the proper way to do it *} |
906 ML {* |
907 ML {* |
907 fun findabs_all rty tm = |
908 fun findabs rty tm = |
|
909 case tm of |
908 case tm of |
910 Abs(_, T, b) => |
909 Abs(_, T, b) => |
911 let |
910 let |
912 val b' = subst_bound ((Free ("x", T)), b); |
911 val b' = subst_bound ((Free ("x", T)), b); |
913 val tys = findabs rty b' |
912 val tys = findabs_all rty b' |
914 val ty = fastype_of tm |
913 val ty = fastype_of tm |
915 in if needs_lift rty ty then (ty :: tys) else tys |
914 in if needs_lift rty ty then (ty :: tys) else tys |
916 end |
915 end |
917 | f $ a => (findabs rty f) @ (findabs rty a) |
916 | f $ a => (findabs_all rty f) @ (findabs_all rty a) |
918 | _ => [] |
917 | _ => []; |
|
918 fun findabs rty tm = distinct (op =) (findabs_all rty tm) |
|
919 *} |
|
920 |
|
921 |
|
922 ML {* |
|
923 fun findaps_all rty tm = |
|
924 case tm of |
|
925 Abs(_, T, b) => |
|
926 findaps_all rty (subst_bound ((Free ("x", T)), b)) |
|
927 | (f $ a) => (findaps_all rty f @ findaps_all rty a) |
|
928 | Free (_, (T as (Type (_, (_ :: _))))) => (if needs_lift rty T then [T] else []) |
|
929 | _ => []; |
|
930 fun findaps rty tm = distinct (op =) (findaps_all rty tm) |
919 *} |
931 *} |
920 |
932 |
921 ML {* |
933 ML {* |
922 fun make_simp_lam_prs_thm lthy quot_thm typ = |
934 fun make_simp_lam_prs_thm lthy quot_thm typ = |
923 let |
935 let |