151 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name |
151 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name |
152 |
152 |
153 (* storing the quot-info *) |
153 (* storing the quot-info *) |
154 val qty_str = fst (Term.dest_Type abs_ty) |
154 val qty_str = fst (Term.dest_Type abs_ty) |
155 val _ = tracing ("storing under: " ^ qty_str) |
155 val _ = tracing ("storing under: " ^ qty_str) |
156 val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
156 val lthy3 = quotdata_update qty_str |
|
157 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
157 (* FIXME: varifyT should not be used *) |
158 (* FIXME: varifyT should not be used *) |
|
159 (* FIXME: the relation needs to be a string, since its type needs *) |
|
160 (* FIXME: to recalculated in for example REGULARIZE *) |
|
161 |
158 (* storing of the equiv_thm under a name *) |
162 (* storing of the equiv_thm under a name *) |
159 val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm) lthy3 |
163 val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm) lthy3 |
160 |
164 |
161 (* interpretation *) |
165 (* interpretation *) |
162 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
166 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |