equal
deleted
inserted
replaced
147 |
147 |
148 (* storing the quot-info *) |
148 (* storing the quot-info *) |
149 val qty_str = fst (dest_Type abs_ty) |
149 val qty_str = fst (dest_Type abs_ty) |
150 val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
150 val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
151 (* FIXME: varifyT should not be used *) |
151 (* FIXME: varifyT should not be used *) |
152 (* the type name maybe should be calculated via qty_name and Sign.intern_type *} |
152 (* the type name maybe should be calculated via qty_name and Sign.intern_type *) |
153 |
153 |
154 (* interpretation *) |
154 (* interpretation *) |
155 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
155 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
156 val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3; |
156 val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3; |
157 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
157 val eqn1i = Thm.prop_of (symmetric eqn1pre) |