140 val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context |
140 val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context |
141 val get_case: Proof.context -> string -> string option list -> RuleCases.T |
141 val get_case: Proof.context -> string -> string option list -> RuleCases.T |
142 val add_notation: Syntax.mode -> (term * mixfix) list -> |
142 val add_notation: Syntax.mode -> (term * mixfix) list -> |
143 Proof.context -> Proof.context |
143 Proof.context -> Proof.context |
144 val expand_abbrevs: bool -> Proof.context -> Proof.context |
144 val expand_abbrevs: bool -> Proof.context -> Proof.context |
145 val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> Proof.context -> |
145 val add_abbrevs: string -> (bstring * term) list -> Proof.context -> |
146 (term * term) list * Proof.context |
146 ((string * typ) * term) list * Proof.context |
147 val verbose: bool ref |
147 val verbose: bool ref |
148 val setmp_verbose: ('a -> 'b) -> 'a -> 'b |
148 val setmp_verbose: ('a -> 'b) -> 'a -> 'b |
149 val print_syntax: Proof.context -> unit |
149 val print_syntax: Proof.context -> unit |
150 val print_binds: Proof.context -> unit |
150 val print_binds: Proof.context -> unit |
151 val print_lthms: Proof.context -> unit |
151 val print_lthms: Proof.context -> unit |
875 |
875 |
876 (* abbreviations *) |
876 (* abbreviations *) |
877 |
877 |
878 val expand_abbrevs = map_consts o apsnd o Consts.expand_abbrevs; |
878 val expand_abbrevs = map_consts o apsnd o Consts.expand_abbrevs; |
879 |
879 |
880 fun add_abbrevs prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn ctxt => |
880 fun add_abbrevs mode = fold_map (fn (c, raw_t) => fn ctxt => |
881 let |
881 let |
882 val (c, mx) = Syntax.const_mixfix raw_c raw_mx; |
|
883 val t0 = cert_term (ctxt |> expand_abbrevs false) raw_t |
882 val t0 = cert_term (ctxt |> expand_abbrevs false) raw_t |
884 handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c); |
883 handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c); |
885 val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0]; |
884 val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0]; |
886 val (((full_c, T), rhs), consts') = consts_of ctxt |
885 val (res, consts') = consts_of ctxt |
887 |> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), true); |
886 |> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode ((c, t), true); |
888 in |
887 in |
889 ctxt |
888 ctxt |
890 |> Variable.declare_term t |
889 |> Variable.declare_term t |
891 |> map_consts (apsnd (K consts')) |
890 |> map_consts (apsnd (K consts')) |
892 |> map_syntax (LocalSyntax.add_modesyntax (theory_of ctxt) |
891 |> pair res |
893 prmode [(false, (Syntax.constN ^ full_c, T, mx))]) |
|
894 |> pair (Const (full_c, T), rhs) |
|
895 end); |
892 end); |
896 |
893 |
897 |
894 |
898 (* fixes *) |
895 (* fixes *) |
899 |
896 |