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 val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation; |
161 fun with_repaired_path f (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy = |
|
162 thy |
|
163 |> Sign.root_path |
|
164 |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1))))) |
|
165 |> f ctr_sugar |
|
166 |> Sign.restore_naming thy; |
|
167 |
|
168 val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path; |
162 |
169 |
163 fun register_ctr_sugar key ctr_sugar = |
170 fun register_ctr_sugar key ctr_sugar = |
164 Local_Theory.declaration {syntax = false, pervasive = true} |
171 Local_Theory.declaration {syntax = false, pervasive = true} |
165 (fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar))) |
172 (fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar))) |
166 #> Local_Theory.background_theory (Ctr_Sugar_Interpretation.data ctr_sugar); |
173 #> Local_Theory.background_theory (Ctr_Sugar_Interpretation.data ctr_sugar); |