equal
deleted
inserted
replaced
161 make_def bind rhs qty mx attr qenv lthy |
161 make_def bind rhs qty mx attr qenv lthy |
162 end |
162 end |
163 |
163 |
164 fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = |
164 fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = |
165 let |
165 let |
166 val qty = (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystr |
166 val qty = Syntax.read_typ lthy qtystr |
167 val prop = (Syntax.check_prop lthy o Syntax.parse_prop lthy) propstr |
167 val prop = Syntax.read_prop lthy propstr |
168 in |
168 in |
169 quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd |
169 quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd |
170 end |
170 end |
171 |
171 |
172 |
172 |