equal
deleted
inserted
replaced
173 fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b) |
173 fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b) |
174 | open_all_all t = ([], t) |
174 | open_all_all t = ([], t) |
175 |
175 |
176 fun split_def ctxt geq = |
176 fun split_def ctxt geq = |
177 let |
177 let |
178 fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq] |
178 fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq] |
179 val (qs, imp) = open_all_all geq |
179 val (qs, imp) = open_all_all geq |
180 |
180 |
181 val gs = Logic.strip_imp_prems imp |
181 val gs = Logic.strip_imp_prems imp |
182 val eq = Logic.strip_imp_concl imp |
182 val eq = Logic.strip_imp_concl imp |
183 |
183 |
212 let |
212 let |
213 val fnames = map (fst o fst) fixes |
213 val fnames = map (fst o fst) fixes |
214 |
214 |
215 fun check geq = |
215 fun check geq = |
216 let |
216 let |
217 fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq] |
217 fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq] |
218 |
218 |
219 val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq |
219 val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq |
220 |
220 |
221 val _ = fname mem fnames |
221 val _ = fname mem fnames |
222 orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames |
222 orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames |