equal
deleted
inserted
replaced
321 (* alias *) |
321 (* alias *) |
322 |
322 |
323 fun gen_alias decl check (b, arg) lthy = |
323 fun gen_alias decl check (b, arg) lthy = |
324 let |
324 let |
325 val (c, reports) = check {proper = true, strict = false} lthy arg; |
325 val (c, reports) = check {proper = true, strict = false} lthy arg; |
326 val _ = Position.reports reports; |
326 val _ = Context_Position.reports lthy reports; |
327 in decl b c lthy end; |
327 in decl b c lthy end; |
328 |
328 |
329 val alias = |
329 val alias = |
330 gen_alias Local_Theory.const_alias (K (K (fn c => (c, [])))); |
330 gen_alias Local_Theory.const_alias (K (K (fn c => (c, [])))); |
331 val alias_cmd = |
331 val alias_cmd = |