137 ((string * attribute list) * (term * term list) list) list -> |
137 ((string * attribute list) * (term * term list) list) list -> |
138 Proof.context -> (bstring * thm list) list * Proof.context |
138 Proof.context -> (bstring * thm list) list * Proof.context |
139 val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context |
139 val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context |
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 expand_abbrevs: bool -> Proof.context -> Proof.context |
|
143 val add_notation: Syntax.mode -> (term * mixfix) list -> |
142 val add_notation: Syntax.mode -> (term * mixfix) list -> |
144 Proof.context -> Proof.context |
143 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: Syntax.mode -> ((bstring * mixfix) * term) list -> Proof.context -> |
146 (term * term) list * Proof.context |
146 (term * 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 |
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 prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn ctxt => |
881 let |
881 let |
882 val (c, mx) = Syntax.const_mixfix raw_c raw_mx; |
882 val (c, mx) = Syntax.const_mixfix raw_c raw_mx; |
883 val _ = no_skolem true c; |
883 val t0 = cert_term (ctxt |> expand_abbrevs false) raw_t |
884 val full_c = full_name ctxt c; |
884 handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c); |
885 val c' = Syntax.constN ^ full_c; |
|
886 val t0 = cert_term (ctxt |> expand_abbrevs false) raw_t; |
|
887 val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0]; |
885 val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0]; |
888 val T = Term.fastype_of t; |
886 val (((full_c, T), rhs), consts') = consts_of ctxt |
889 val _ = |
887 |> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), true); |
890 if null (Variable.hidden_polymorphism t T) then () |
|
891 else error ("Extra type variables on rhs of abbreviation: " ^ quote c); |
|
892 in |
888 in |
893 ctxt |
889 ctxt |
894 |> Variable.declare_term t |
890 |> Variable.declare_term t |
895 |> map_consts (apsnd |
891 |> map_consts (apsnd (K consts')) |
896 (Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), true))) |
892 |> map_syntax (LocalSyntax.add_modesyntax (theory_of ctxt) |
897 |> map_syntax (LocalSyntax.add_modesyntax (theory_of ctxt) prmode [(false, (c', T, mx))]) |
893 prmode [(false, (Syntax.constN ^ full_c, T, mx))]) |
898 |> pair (Const (full_c, T), t) |
894 |> pair (Const (full_c, T), rhs) |
899 end); |
895 end); |
900 |
896 |
901 |
897 |
902 (* fixes *) |
898 (* fixes *) |
903 |
899 |