# HG changeset patch
# User wenzelm
# Date 1165436338 -3600
# Node ID 8b8edcdb4da84cbd8427de8feb15633644ecb83f
# Parent  5d2230ad12610ccc1aae3ad17043444e6d3f629c
add_abbrevs: moved common parts to consts.ML;

diff -r 5d2230ad1261 -r 8b8edcdb4da8 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Dec 06 21:18:57 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Dec 06 21:18:58 2006 +0100
@@ -139,9 +139,9 @@
   val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
   val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
   val get_case: Proof.context -> string -> string option list -> RuleCases.T
-  val expand_abbrevs: bool -> Proof.context -> Proof.context
   val add_notation: Syntax.mode -> (term * mixfix) list ->
     Proof.context -> Proof.context
+  val expand_abbrevs: bool -> Proof.context -> Proof.context
   val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> Proof.context ->
     (term * term) list * Proof.context
   val verbose: bool ref
@@ -880,22 +880,18 @@
 fun add_abbrevs prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn ctxt =>
   let
     val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
-    val _ = no_skolem true c;
-    val full_c = full_name ctxt c;
-    val c' = Syntax.constN ^ full_c;
-    val t0 = cert_term (ctxt |> expand_abbrevs false) raw_t;
+    val t0 = cert_term (ctxt |> expand_abbrevs false) raw_t
+      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
     val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
-    val T = Term.fastype_of t;
-    val _ =
-      if null (Variable.hidden_polymorphism t T) then ()
-      else error ("Extra type variables on rhs of abbreviation: " ^ quote c);
+    val (((full_c, T), rhs), consts') = consts_of ctxt
+      |> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), true);
   in
     ctxt
     |> Variable.declare_term t
-    |> map_consts (apsnd
-      (Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), true)))
-    |> map_syntax (LocalSyntax.add_modesyntax (theory_of ctxt) prmode [(false, (c', T, mx))])
-    |> pair (Const (full_c, T), t)
+    |> map_consts (apsnd (K consts'))
+    |> map_syntax (LocalSyntax.add_modesyntax (theory_of ctxt)
+      prmode [(false, (Syntax.constN ^ full_c, T, mx))])
+    |> pair (Const (full_c, T), rhs)
   end);
 
 
diff -r 5d2230ad1261 -r 8b8edcdb4da8 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Dec 06 21:18:57 2006 +0100
+++ b/src/Pure/sign.ML	Wed Dec 06 21:18:58 2006 +0100
@@ -751,25 +751,21 @@
 end;
 
 
-(* add abbreviations -- cf. Sign.add_abbrevs *)
+(* add abbreviations -- cf. ProofContext.add_abbrevs *)
 
 fun add_abbrevs prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn thy =>
   let
-    val prep_tm = Compress.term thy o Logic.varify o no_vars (pp thy) o
-      Term.no_dummy_patterns o cert_term_abbrev thy;
-
     val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
-    val full_c = full_name thy c;
-    val c' = Syntax.constN ^ full_c;
+    val prep_tm = Compress.term thy o Term.no_dummy_patterns o cert_term_abbrev thy;
     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
-    val T = Term.fastype_of t;
+    val (((full_c, T), rhs), consts') = consts_of thy
+      |> Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) (#1 prmode) ((c, t), true);
   in
     thy
-    |> map_consts
-      (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) (#1 prmode) ((c, t), true))
-    |> add_modesyntax_i prmode [(c', T, mx)]
-    |> pair (Const (full_c, T), t)
+    |> map_consts (K consts')
+    |> add_modesyntax_i prmode [(Syntax.constN ^ full_c, T, mx)]
+    |> pair (Const (full_c, T), rhs)
   end);