equal
deleted
inserted
replaced
148 (* - a meta-equation defining the constant, *) |
148 (* - a meta-equation defining the constant, *) |
149 (* and the attributes of for this meta-equality *) |
149 (* and the attributes of for this meta-equality *) |
150 |
150 |
151 fun quotdef ((bind, qty, mx), (attr, prop)) lthy = |
151 fun quotdef ((bind, qty, mx), (attr, prop)) lthy = |
152 let |
152 let |
153 val (_, prop') = PrimitiveDefs.dest_def lthy (K true) (K false) (K false) prop |
153 val (_, prop') = Primitive_Defs.dest_def lthy (K true) (K false) (K false) prop |
154 val (_, rhs) = PrimitiveDefs.abs_def prop' |
154 val (_, rhs) = Primitive_Defs.abs_def prop' |
155 in |
155 in |
156 make_def bind qty mx attr rhs lthy |
156 make_def bind qty mx attr rhs lthy |
157 end |
157 end |
158 |
158 |
159 fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = |
159 fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = |