# HG changeset patch
# User haftmann
# Date 1281444821 -7200
# Node ID 9dd57db3c0f25b352fcd2653852169cd825fe6b0
# Parent  228566e1ab00ed918adb9a22f05a40beb5c104f8
moved extra_tfrees check for mixfix syntax to Generic_Target

diff -r 228566e1ab00 -r 9dd57db3c0f2 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Aug 10 14:47:22 2010 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Aug 10 14:53:41 2010 +0200
@@ -8,7 +8,7 @@
 signature GENERIC_TARGET =
 sig
   val define: (((binding * typ) * mixfix) * (binding * term) -> term list
-    -> (string * sort) list * term list -> local_theory -> (term * thm) * local_theory)
+    -> term list -> local_theory -> (term * thm) * local_theory)
     -> (binding * mixfix) * (Attrib.binding * term) -> local_theory
     -> (term * (string * thm)) * local_theory
   val notes: (string
@@ -18,7 +18,7 @@
     -> string -> (Attrib.binding * (thm list * Args.src list) list) list
     -> local_theory -> (string * thm list) list * local_theory
   val abbrev: (string * bool -> binding * mixfix -> term * term
-    -> (string * sort) list * term list -> local_theory -> local_theory)
+    -> term list -> local_theory -> local_theory)
     -> string * bool -> (binding * mixfix) * term -> local_theory
     -> (term * term) * local_theory
 end;
@@ -26,6 +26,19 @@
 structure Generic_Target: GENERIC_TARGET =
 struct
 
+(* mixfix syntax *)
+
+fun check_mixfix ctxt (b, extra_tfrees) 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);
+
+
 (* define *)
 
 fun define foundation ((b, mx), ((proto_b_def, atts), rhs)) lthy =
@@ -44,6 +57,7 @@
     val T = Term.fastype_of rhs;
     val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);
     val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs []));
+    val mx' = check_mixfix lthy (b, extra_tfrees) mx;
 
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
     val term_params =
@@ -58,7 +72,7 @@
 
     (*foundation*)
     val ((lhs', global_def), lthy3) = foundation
-      (((b, U), mx), (b_def, rhs')) params (extra_tfrees, type_params) lthy;
+      (((b, U), mx'), (b_def, rhs')) params type_params lthy;
 
     (*local definition*)
     val ((lhs, local_def), lthy4) = lthy3
@@ -151,12 +165,13 @@
 
     val extra_tfrees =
       subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
+    val mx' = check_mixfix lthy (b, extra_tfrees) mx;
 
     val global_rhs =
       singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
   in
     lthy
-    |> target_abbrev prmode (b, mx) (global_rhs, t') (extra_tfrees, xs)
+    |> target_abbrev prmode (b, mx') (global_rhs, t') xs
     |> ProofContext.add_abbrev Print_Mode.internal (b, t) |> snd
     |> Local_Defs.fixed_abbrev ((b, NoSyn), t)
   end;
diff -r 228566e1ab00 -r 9dd57db3c0f2 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Aug 10 14:47:22 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Tue Aug 10 14:53:41 2010 +0200
@@ -109,30 +109,11 @@
 
 (* 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;
-
 
 (* define *)
 
@@ -141,9 +122,9 @@
 fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
 
 fun foundation (ta as Target {target, is_locale, is_class, ...})
-    (((b, U), mx), (b_def, rhs')) params (extra_tfrees, type_params) lthy =
+    (((b, U), mx), (b_def, rhs')) params type_params lthy =
   let
-    val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
+    val (mx1, mx2, mx3) = fork_mixfix ta mx;
     val (const, lthy2) = lthy |>
       (case Class_Target.instantiation_param lthy b of
         SOME c' =>
@@ -221,9 +202,9 @@
       ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
 
 fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
-    prmode (b, mx) (global_rhs, t') (extra_tfrees, xs) lthy =
+    prmode (b, mx) (global_rhs, t') xs lthy =
   let
-    val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
+    val (mx1, mx2, mx3) = fork_mixfix ta mx;
   in if is_locale
     then lthy
       |> locale_abbrev ta prmode ((b, mx2), global_rhs) xs