equal
deleted
inserted
replaced
275 let |
275 let |
276 (* new parsing with proper declaration *) |
276 (* new parsing with proper declaration *) |
277 val rty = Syntax.read_typ lthy rty_str |
277 val rty = Syntax.read_typ lthy rty_str |
278 val lthy1 = Variable.declare_typ rty lthy |
278 val lthy1 = Variable.declare_typ rty lthy |
279 val rel = |
279 val rel = |
280 Syntax.parse_term lthy1 rel_str |
280 Syntax.parse_term lthy1 rel_str |
281 |> Syntax.type_constraint (rty --> rty --> @{typ bool}) |
281 |> Syntax.type_constraint (rty --> rty --> @{typ bool}) |
282 |> Syntax.check_term lthy1 |
282 |> Syntax.check_term lthy1 |
283 val lthy2 = Variable.declare_term rel lthy1 |
283 val lthy2 = Variable.declare_term rel lthy1 |
284 in |
284 in |
285 (((vs, qty_name, mx), (rty, rel)), lthy2) |
285 (((vs, qty_name, mx), (rty, rel)), lthy2) |
286 end |
286 end |
287 |
287 |