# HG changeset patch
# User wenzelm
# Date 1275659293 -7200
# Node ID f5abedb7aed5fbf208e078401f023ae661586ae3
# Parent  715d25555ca6817a1abcec7eb7039726b90062dc
more robust handling of additional type variables: warning, more canonical order, drop mixfix syntax if implicit type arguments are introduced (to avoid delusion due to shifted arguments);

diff -r 715d25555ca6 -r f5abedb7aed5 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Fri Jun 04 14:15:56 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Fri Jun 04 15:48:13 2010 +0200
@@ -180,13 +180,35 @@
   end;
 
 
-(* consts *)
+(* mixfix notation *)
+
+local
 
 fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
   if not is_locale then (NoSyn, NoSyn, mx)
   else if not is_class then (NoSyn, mx, NoSyn)
   else (mx, NoSyn, NoSyn);
 
+in
+
+fun prep_mixfix ctxt ta (b, extra_tfrees) mx =
+  let
+    val mx' =
+      if null extra_tfrees then mx
+      else
+        (warning
+          ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^
+            commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
+            (if mx = NoSyn then ""
+             else "\nDropping mixfix syntax " ^ Pretty.string_of (Syntax.pretty_mixfix mx)));
+          NoSyn);
+  in fork_mixfix ta mx' end;
+
+end;
+
+
+(* consts *)
+
 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
   let
     val b' = Morphism.binding phi b;
@@ -218,10 +240,14 @@
     val thy_ctxt = ProofContext.init_global (ProofContext.theory_of lthy);
     val target_ctxt = Local_Theory.target_of lthy;
 
-    val (mx1, mx2, mx3) = fork_mixfix ta mx;
     val t' = Assumption.export_term lthy target_ctxt t;
     val xs = map Free (rev (Variable.add_fixed target_ctxt t' []));
     val u = fold_rev lambda xs t';
+
+    val extra_tfrees =
+      subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
+    val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
+
     val global_rhs =
       singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
   in
@@ -261,7 +287,7 @@
     val params = type_params @ term_params;
 
     val U = map Term.fastype_of params ---> T;
-    val (mx1, mx2, mx3) = fork_mixfix ta mx;
+    val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
     val (const, lthy') = lthy |>
       (case Class_Target.instantiation_param lthy b of
         SOME c' =>
@@ -299,10 +325,7 @@
     val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
     val T = Term.fastype_of rhs;
     val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);
-    val extra_tfrees =
-      fold_types (fold_atyps
-        (fn TFree v => if member (op =) tfreesT v then I else insert (op =) v | _ => I)) rhs []
-      |> sort_wrt #1;
+    val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs []));
 
     (*const*)
     val ((lhs, local_def), lthy2) = lthy |> declare_const ta extra_tfrees xs ((b, T), mx);