equal
deleted
inserted
replaced
156 ( |
156 ( |
157 type T = ctr_sugar; |
157 type T = ctr_sugar; |
158 val eq: T * T -> bool = op = o pairself #ctrs; |
158 val eq: T * T -> bool = op = o pairself #ctrs; |
159 ); |
159 ); |
160 |
160 |
161 (* FIXME naming *) |
|
162 fun with_repaired_path f (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy = |
161 fun with_repaired_path f (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy = |
163 thy |
162 thy |
164 (*|> Sign.root_path*) |
163 |> Sign.root_path |
165 |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1))))) |
164 |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1))))) |
166 (*|> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy)*) |
165 |> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy) |
167 (*|> Sign.restore_naming thy*); |
166 |> Sign.restore_naming thy; |
168 |
167 |
169 fun ctr_sugar_interpretation f = Ctr_Sugar_Interpretation.interpretation (with_repaired_path f); |
168 fun ctr_sugar_interpretation f = Ctr_Sugar_Interpretation.interpretation (with_repaired_path f); |
170 |
169 |
171 fun register_ctr_sugar key ctr_sugar = |
170 fun register_ctr_sugar key ctr_sugar = |
172 Local_Theory.declaration {syntax = false, pervasive = true} |
171 Local_Theory.declaration {syntax = false, pervasive = true} |