equal
deleted
inserted
replaced
150 ML {* maps_lookup @{theory} "fun" *} |
150 ML {* maps_lookup @{theory} "fun" *} |
151 |
151 |
152 ML {* |
152 ML {* |
153 val quot_def_parser = |
153 val quot_def_parser = |
154 (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- |
154 (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- |
155 ((OuterParse.list1 OuterParse.binding) --| OuterParse.$$$ ")")) -- |
155 ((OuterParse.list1 OuterParse.typ) --| OuterParse.$$$ ")")) -- |
156 (OuterParse.binding -- |
156 (OuterParse.binding -- |
157 Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) -- |
157 Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) -- |
158 OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec) |
158 OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec) |
159 *} |
159 *} |
160 |
160 |