94 fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts'); |
94 fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts'); |
95 |
95 |
96 fun map_ctxt {binding, typ, term, pattern, fact, attrib} = |
96 fun map_ctxt {binding, typ, term, pattern, fact, attrib} = |
97 fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx))) |
97 fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx))) |
98 | Constrains xs => Constrains (xs |> map (fn (x, T) => |
98 | Constrains xs => Constrains (xs |> map (fn (x, T) => |
99 (Binding.base_name (binding (Binding.name x)), typ T))) |
99 (Binding.name_of (binding (Binding.name x)), typ T))) |
100 | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) => |
100 | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) => |
101 ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps))))) |
101 ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps))))) |
102 | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => |
102 | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => |
103 ((binding a, map attrib atts), (term t, map pattern ps)))) |
103 ((binding a, map attrib atts), (term t, map pattern ps)))) |
104 | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) => |
104 | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) => |
141 |
141 |
142 fun prt_show (a, ts) = |
142 fun prt_show (a, ts) = |
143 Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts))); |
143 Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts))); |
144 |
144 |
145 fun prt_var (x, SOME T) = Pretty.block |
145 fun prt_var (x, SOME T) = Pretty.block |
146 [Pretty.str (Binding.base_name x ^ " ::"), Pretty.brk 1, prt_typ T] |
146 [Pretty.str (Binding.name_of x ^ " ::"), Pretty.brk 1, prt_typ T] |
147 | prt_var (x, NONE) = Pretty.str (Binding.base_name x); |
147 | prt_var (x, NONE) = Pretty.str (Binding.name_of x); |
148 val prt_vars = separate (Pretty.keyword "and") o map prt_var; |
148 val prt_vars = separate (Pretty.keyword "and") o map prt_var; |
149 |
149 |
150 fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts)) |
150 fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts)) |
151 | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks |
151 | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks |
152 (prt_vars xs @ [Pretty.keyword "where"] @ prt_terms ts)); |
152 (prt_vars xs @ [Pretty.keyword "where"] @ prt_terms ts)); |
166 val prt_name_atts = pretty_name_atts ctxt; |
166 val prt_name_atts = pretty_name_atts ctxt; |
167 |
167 |
168 fun prt_mixfix NoSyn = [] |
168 fun prt_mixfix NoSyn = [] |
169 | prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx]; |
169 | prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx]; |
170 |
170 |
171 fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.base_name x ^ " ::") :: |
171 fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.name_of x ^ " ::") :: |
172 Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx) |
172 Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx) |
173 | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.base_name x) :: |
173 | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.name_of x) :: |
174 Pretty.brk 1 :: prt_mixfix mx); |
174 Pretty.brk 1 :: prt_mixfix mx); |
175 fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn); |
175 fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn); |
176 |
176 |
177 fun prt_asm (a, ts) = |
177 fun prt_asm (a, ts) = |
178 Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts)); |
178 Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts)); |
500 | activate_elem (Defines defs) ctxt = |
500 | activate_elem (Defines defs) ctxt = |
501 let |
501 let |
502 val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; |
502 val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; |
503 val asms = defs' |> map (fn ((name, atts), (t, ps)) => |
503 val asms = defs' |> map (fn ((name, atts), (t, ps)) => |
504 let val ((c, _), t') = LocalDefs.cert_def ctxt t |
504 let val ((c, _), t') = LocalDefs.cert_def ctxt t |
505 in (t', ((Binding.map_base (Thm.def_name_optional c) name, atts), [(t', ps)])) end); |
505 in (t', ((Binding.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end); |
506 val (_, ctxt') = |
506 val (_, ctxt') = |
507 ctxt |> fold (Variable.auto_fixes o #1) asms |
507 ctxt |> fold (Variable.auto_fixes o #1) asms |
508 |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms); |
508 |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms); |
509 in ctxt' end |
509 in ctxt' end |
510 | activate_elem (Notes (kind, facts)) ctxt = |
510 | activate_elem (Notes (kind, facts)) ctxt = |