equal
deleted
inserted
replaced
69 VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn] |
69 VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn] |
70 **) |
70 **) |
71 fun get_vars c = |
71 fun get_vars c = |
72 let |
72 let |
73 val d = Logic.strip_assums_concl c; |
73 val d = Logic.strip_assums_concl c; |
74 val Const _ $ pre $ _ $ _ = HOLogic.dest_Trueprop d; |
74 val Const _ $ pre $ _ $ _ $ _ = HOLogic.dest_Trueprop d; |
75 in mk_vars pre end; |
75 in mk_vars pre end; |
76 |
76 |
77 fun mk_CollectC tm = |
77 fun mk_CollectC tm = |
78 let val \<^Type>\<open>fun t _\<close> = fastype_of tm; |
78 let val \<^Type>\<open>fun t _\<close> = fastype_of tm; |
79 in \<^Const>\<open>Collect t for tm\<close> end; |
79 in \<^Const>\<open>Collect t for tm\<close> end; |