equal
deleted
inserted
replaced
246 (* notation *) |
246 (* notation *) |
247 |
247 |
248 fun type_notation add mode raw_args lthy = |
248 fun type_notation add mode raw_args lthy = |
249 let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args in |
249 let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args in |
250 declaration {syntax = true, pervasive = false} |
250 declaration {syntax = true, pervasive = false} |
251 (Proof_Context.target_type_notation add mode args) lthy |
251 (Proof_Context.generic_type_notation add mode args) lthy |
252 end; |
252 end; |
253 |
253 |
254 fun notation add mode raw_args lthy = |
254 fun notation add mode raw_args lthy = |
255 let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args in |
255 let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args in |
256 declaration {syntax = true, pervasive = false} |
256 declaration {syntax = true, pervasive = false} |
257 (Proof_Context.target_notation add mode args) lthy |
257 (Proof_Context.generic_notation add mode args) lthy |
258 end; |
258 end; |
259 |
259 |
260 |
260 |
261 (* name space aliases *) |
261 (* name space aliases *) |
262 |
262 |