equal
deleted
inserted
replaced
116 |
116 |
117 fun quotdef ((bind, qty, mx), (attr, prop)) lthy = |
117 fun quotdef ((bind, qty, mx), (attr, prop)) lthy = |
118 let |
118 let |
119 val (_, prop') = LocalDefs.cert_def lthy prop |
119 val (_, prop') = LocalDefs.cert_def lthy prop |
120 val (_, rhs) = Primitive_Defs.abs_def prop' |
120 val (_, rhs) = Primitive_Defs.abs_def prop' |
121 in |
121 in |
122 make_def bind qty mx attr rhs lthy |
122 make_def bind qty mx attr rhs lthy |
123 end |
123 end |
124 |
124 |
125 fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = |
125 fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = |
126 let |
126 let |