149 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
149 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
150 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name |
150 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name |
151 |
151 |
152 (* storing the quot-info *) |
152 (* storing the quot-info *) |
153 val qty_str = fst (Term.dest_Type abs_ty) |
153 val qty_str = fst (Term.dest_Type abs_ty) |
154 val _ = tracing ("storing under: " ^ qty_str) |
|
155 val lthy3 = quotdata_update qty_str |
154 val lthy3 = quotdata_update qty_str |
156 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
155 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
157 (* FIXME: varifyT should not be used *) |
156 (* FIXME: varifyT should not be used *) |
158 (* FIXME: the relation needs to be a string, since its type needs *) |
157 (* FIXME: the relation needs to be a string, since its type needs *) |
159 (* FIXME: to recalculated in for example REGULARIZE *) |
158 (* FIXME: to recalculated in for example REGULARIZE *) |