equal
deleted
inserted
replaced
180 Const _ $ Abs _ => dest_cabs (Thm.dest_arg ct) ctxt |
180 Const _ $ Abs _ => dest_cabs (Thm.dest_arg ct) ctxt |
181 | _ => raise CTERM ("not a binder", [ct])) |
181 | _ => raise CTERM ("not a binder", [ct])) |
182 |
182 |
183 val dest_all_cbinders = repeat_yield (try o dest_cbinder) |
183 val dest_all_cbinders = repeat_yield (try o dest_cbinder) |
184 |
184 |
185 val mk_cprop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop}) |
185 val mk_cprop = Thm.apply (Thm.cterm_of @{theory} @{const Trueprop}) |
186 |
186 |
187 fun dest_cprop ct = |
187 fun dest_cprop ct = |
188 (case Thm.term_of ct of |
188 (case Thm.term_of ct of |
189 @{const Trueprop} $ _ => Thm.dest_arg ct |
189 @{const Trueprop} $ _ => Thm.dest_arg ct |
190 | _ => raise CTERM ("not a property", [ct])) |
190 | _ => raise CTERM ("not a property", [ct])) |