equal
deleted
inserted
replaced
140 |
140 |
141 fun check_format ctxt st = |
141 fun check_format ctxt st = |
142 let |
142 let |
143 val concl' = Logic.strip_assums_concl (hd (prems_of st)) |
143 val concl' = Logic.strip_assums_concl (hd (prems_of st)) |
144 val concl = HOLogic.dest_Trueprop concl' |
144 val concl = HOLogic.dest_Trueprop concl' |
145 val expr = fst (strip_comb (fst (PredicateCompFuns.dest_Eval concl))) |
145 val expr = fst (strip_comb (fst (Predicate_Comp_Funs.dest_Eval concl))) |
146 fun valid_expr (Const (@{const_name Predicate.bind}, _)) = true |
146 fun valid_expr (Const (@{const_name Predicate.bind}, _)) = true |
147 | valid_expr (Const (@{const_name Predicate.single}, _)) = true |
147 | valid_expr (Const (@{const_name Predicate.single}, _)) = true |
148 | valid_expr _ = false |
148 | valid_expr _ = false |
149 in |
149 in |
150 if valid_expr expr then |
150 if valid_expr expr then |