add_abbrevs: moved common parts to consts.ML;
authorwenzelm
Wed Dec 06 21:18:58 2006 +0100 (2006-12-06)
changeset 216818b8edcdb4da8
parent 21680 5d2230ad1261
child 21682 53c9a026fcb7
add_abbrevs: moved common parts to consts.ML;
src/Pure/Isar/proof_context.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Dec 06 21:18:57 2006 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Dec 06 21:18:58 2006 +0100
     1.3 @@ -139,9 +139,9 @@
     1.4    val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
     1.5    val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
     1.6    val get_case: Proof.context -> string -> string option list -> RuleCases.T
     1.7 -  val expand_abbrevs: bool -> Proof.context -> Proof.context
     1.8    val add_notation: Syntax.mode -> (term * mixfix) list ->
     1.9      Proof.context -> Proof.context
    1.10 +  val expand_abbrevs: bool -> Proof.context -> Proof.context
    1.11    val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> Proof.context ->
    1.12      (term * term) list * Proof.context
    1.13    val verbose: bool ref
    1.14 @@ -880,22 +880,18 @@
    1.15  fun add_abbrevs prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn ctxt =>
    1.16    let
    1.17      val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
    1.18 -    val _ = no_skolem true c;
    1.19 -    val full_c = full_name ctxt c;
    1.20 -    val c' = Syntax.constN ^ full_c;
    1.21 -    val t0 = cert_term (ctxt |> expand_abbrevs false) raw_t;
    1.22 +    val t0 = cert_term (ctxt |> expand_abbrevs false) raw_t
    1.23 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
    1.24      val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
    1.25 -    val T = Term.fastype_of t;
    1.26 -    val _ =
    1.27 -      if null (Variable.hidden_polymorphism t T) then ()
    1.28 -      else error ("Extra type variables on rhs of abbreviation: " ^ quote c);
    1.29 +    val (((full_c, T), rhs), consts') = consts_of ctxt
    1.30 +      |> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), true);
    1.31    in
    1.32      ctxt
    1.33      |> Variable.declare_term t
    1.34 -    |> map_consts (apsnd
    1.35 -      (Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), true)))
    1.36 -    |> map_syntax (LocalSyntax.add_modesyntax (theory_of ctxt) prmode [(false, (c', T, mx))])
    1.37 -    |> pair (Const (full_c, T), t)
    1.38 +    |> map_consts (apsnd (K consts'))
    1.39 +    |> map_syntax (LocalSyntax.add_modesyntax (theory_of ctxt)
    1.40 +      prmode [(false, (Syntax.constN ^ full_c, T, mx))])
    1.41 +    |> pair (Const (full_c, T), rhs)
    1.42    end);
    1.43  
    1.44  
     2.1 --- a/src/Pure/sign.ML	Wed Dec 06 21:18:57 2006 +0100
     2.2 +++ b/src/Pure/sign.ML	Wed Dec 06 21:18:58 2006 +0100
     2.3 @@ -751,25 +751,21 @@
     2.4  end;
     2.5  
     2.6  
     2.7 -(* add abbreviations -- cf. Sign.add_abbrevs *)
     2.8 +(* add abbreviations -- cf. ProofContext.add_abbrevs *)
     2.9  
    2.10  fun add_abbrevs prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn thy =>
    2.11    let
    2.12 -    val prep_tm = Compress.term thy o Logic.varify o no_vars (pp thy) o
    2.13 -      Term.no_dummy_patterns o cert_term_abbrev thy;
    2.14 -
    2.15      val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
    2.16 -    val full_c = full_name thy c;
    2.17 -    val c' = Syntax.constN ^ full_c;
    2.18 +    val prep_tm = Compress.term thy o Term.no_dummy_patterns o cert_term_abbrev thy;
    2.19      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    2.20        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
    2.21 -    val T = Term.fastype_of t;
    2.22 +    val (((full_c, T), rhs), consts') = consts_of thy
    2.23 +      |> Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) (#1 prmode) ((c, t), true);
    2.24    in
    2.25      thy
    2.26 -    |> map_consts
    2.27 -      (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) (#1 prmode) ((c, t), true))
    2.28 -    |> add_modesyntax_i prmode [(c', T, mx)]
    2.29 -    |> pair (Const (full_c, T), t)
    2.30 +    |> map_consts (K consts')
    2.31 +    |> add_modesyntax_i prmode [(Syntax.constN ^ full_c, T, mx)]
    2.32 +    |> pair (Const (full_c, T), rhs)
    2.33    end);
    2.34  
    2.35