# HG changeset patch
# User wenzelm
# Date 1333462234 -7200
# Node ID 6a641856a0e9a5069380c674c4a4aced204c9ae6
# Parent  ba9c8613ad9bd8774625fd6a5e9b4bd200474535
better drop background syntax if entity depends on parameters;
more direct Type_Infer_Context.const_type instead of Syntax.check_term, which expands abbreviations (and potentially more);

diff -r ba9c8613ad9b -r 6a641856a0e9 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Apr 03 14:37:16 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Apr 03 16:10:34 2012 +0200
@@ -60,6 +60,11 @@
          else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)));
       NoSyn);
 
+fun check_mixfix_global (b, no_params) mx =
+  if no_params orelse mx = NoSyn then mx
+  else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
+    Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn);
+
 
 (* define *)
 
@@ -236,13 +241,10 @@
             let
               val thy = Context.theory_of context;
               val ctxt = Context.proof_of context;
-              val t' = Syntax.check_term ctxt (Const (c, dummyT))
-                |> singleton (Variable.polymorphic ctxt);
             in
-              (case t' of
-                Const (c', T') =>
-                  if c = c' andalso Sign.typ_equiv thy (T, T') then SOME c else NONE
-              | _ => NONE)
+              (case Type_Infer_Context.const_type ctxt c of
+                SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE
+              | NONE => NONE)
             end
         | _ => NONE)
       else NONE;
@@ -274,9 +276,13 @@
 
 fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   let
+    val params = type_params @ term_params;
+    val mx' = check_mixfix_global (b, null params) mx;
+
     val (const, lthy2) = lthy
-      |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx));
-    val lhs = list_comb (const, type_params @ term_params);
+      |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx'));
+    val lhs = Term.list_comb (const, params);
+
     val ((_, def), lthy3) = lthy2
       |> Local_Theory.background_theory_result
         (Thm.add_def lthy2 false false
@@ -301,7 +307,8 @@
 fun theory_abbrev prmode (b, mx) (t, _) xs =
   Local_Theory.background_theory_result
     (Sign.add_abbrev (#1 prmode) (b, t) #->
-      (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)] #> pair lhs))
+      (fn (lhs, _) =>  (* FIXME type_params!? *)
+        Sign.notation true prmode [(lhs, check_mixfix_global (b, null xs) mx)] #> pair lhs))
   #-> (fn lhs => fn lthy' => lthy' |>
         const_declaration (fn level => level <> Local_Theory.level lthy') prmode
           ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
diff -r ba9c8613ad9b -r 6a641856a0e9 src/Pure/type_infer_context.ML
--- a/src/Pure/type_infer_context.ML	Tue Apr 03 14:37:16 2012 +0200
+++ b/src/Pure/type_infer_context.ML	Tue Apr 03 16:10:34 2012 +0200
@@ -7,6 +7,7 @@
 signature TYPE_INFER_CONTEXT =
 sig
   val const_sorts: bool Config.T
+  val const_type: Proof.context -> string -> typ option
   val prepare_positions: Proof.context -> term list -> term list * (Position.T * typ) list
   val prepare: Proof.context -> term list -> int * term list
   val infer_types: Proof.context -> term list -> term list