23 type context_i (*= (typ, term, thm list) ctxt*) |
23 type context_i (*= (typ, term, thm list) ctxt*) |
24 val map_ctxt: {name: string -> string, |
24 val map_ctxt: {name: string -> string, |
25 var: string * mixfix -> string * mixfix, |
25 var: string * mixfix -> string * mixfix, |
26 typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c, |
26 typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c, |
27 attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt |
27 attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt |
|
28 val map_ctxt_attrib: (Attrib.src -> Attrib.src) -> |
|
29 ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt |
28 val morph_ctxt: morphism -> context_i -> context_i |
30 val morph_ctxt: morphism -> context_i -> context_i |
29 val params_of: context_i -> (string * typ) list |
31 val params_of: context_i -> (string * typ) list |
30 val prems_of: context_i -> term list |
32 val prems_of: context_i -> term list |
31 val facts_of: theory -> context_i -> |
33 val facts_of: theory -> context_i -> |
32 ((string * Attrib.src list) * (thm list * Attrib.src list) list) list |
34 ((string * Attrib.src list) * (thm list * Attrib.src list) list) list |
107 | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => |
109 | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => |
108 ((name a, map attrib atts), (term t, map term ps)))) |
110 ((name a, map attrib atts), (term t, map term ps)))) |
109 | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) => |
111 | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) => |
110 ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts))))); |
112 ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts))))); |
111 |
113 |
|
114 fun map_ctxt_attrib attrib = |
|
115 map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = attrib}; |
|
116 |
112 fun morph_ctxt phi = map_ctxt |
117 fun morph_ctxt phi = map_ctxt |
113 {name = Morphism.name phi, |
118 {name = Morphism.name phi, |
114 var = Morphism.var phi, |
119 var = Morphism.var phi, |
115 typ = Morphism.typ phi, |
120 typ = Morphism.typ phi, |
116 term = Morphism.term phi, |
121 term = Morphism.term phi, |