merged

--- a/NEWS	Sat Mar 13 17:05:34 2010 -0800
+++ b/NEWS	Sat Mar 13 17:36:53 2010 -0800
@@ -64,6 +64,12 @@
 
 *** Pure ***
 
+* Local theory specifications may depend on extra type variables that
+are not present in the result type -- arguments TYPE('a) :: 'a itself
+are added internally.  For example:
+
+  definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"
+
 * Code generator: details of internal data cache have no impact on
 the user space functionality any longer.
 

--- a/src/HOL/Tools/typedef.ML	Sat Mar 13 17:05:34 2010 -0800
+++ b/src/HOL/Tools/typedef.ML	Sat Mar 13 17:36:53 2010 -0800
@@ -158,22 +158,11 @@
 
     (* set definition *)
 
-    (* FIXME let Local_Theory.define handle hidden polymorphism (!??!) *)
-
-    val rhs_tfrees = Term.add_tfrees set [];
-    val rhs_tfreesT = Term.add_tfreesT setT [];
-
-    val set_argsT = lhs_tfrees
-      |> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT))
-      |> map TFree;
-    val set_args = map Logic.mk_type set_argsT;
-
     val ((set', set_def), set_lthy) =
       if def_set then
         typedecl_lthy
-        |> Local_Theory.define
-          ((name, NoSyn), ((Thm.def_binding name, []), fold_rev lambda set_args set))
-        |>> (fn (s, (_, set_def)) => (Term.list_comb (s, set_args), SOME set_def))
+        |> Local_Theory.define ((name, NoSyn), ((Thm.def_binding name, []), set))
+        |>> (fn (set', (_, set_def)) => (set', SOME set_def))
       else ((set, NONE), typedecl_lthy);
 
 

--- a/src/Pure/Isar/args.ML	Sat Mar 13 17:05:34 2010 -0800
+++ b/src/Pure/Isar/args.ML	Sat Mar 13 17:36:53 2010 -0800
@@ -14,7 +14,6 @@
   val pretty_src: Proof.context -> src -> Pretty.T
   val map_name: (string -> string) -> src -> src
   val morph_values: morphism -> src -> src
-  val maxidx_values: src -> int -> int
   val assignable: src -> src
   val closure: src -> src
   val context: Proof.context context_parser
@@ -111,13 +110,6 @@
     | T.Fact ths => T.Fact (Morphism.fact phi ths)
     | T.Attribute att => T.Attribute (Morphism.transform phi att)));
 
-fun maxidx_values (Src ((_, args), _)) = args |> fold (fn arg =>
-  (case T.get_value arg of
-    SOME (T.Typ T) => Term.maxidx_typ T
-  | SOME (T.Term t) => Term.maxidx_term t
-  | SOME (T.Fact ths) => fold Thm.maxidx_thm ths
-  | _ => I));
-
 val assignable = map_args T.assignable;
 val closure = map_args T.closure;
 

--- a/src/Pure/Isar/element.ML	Sat Mar 13 17:05:34 2010 -0800
+++ b/src/Pure/Isar/element.ML	Sat Mar 13 17:36:53 2010 -0800
@@ -55,9 +55,6 @@
   val satisfy_facts: witness list ->
     (Attrib.binding * (thm list * Attrib.src list) list) list ->
     (Attrib.binding * (thm list * Attrib.src list) list) list
-  val generalize_facts: Proof.context -> Proof.context ->
-    (Attrib.binding * (thm list * Attrib.src list) list) list ->
-    (Attrib.binding * (thm list * Attrib.src list) list) list
   val eq_morphism: theory -> thm list -> morphism
   val transfer_morphism: theory -> morphism
   val init: context_i -> Context.generic -> Context.generic
@@ -458,22 +455,6 @@
   fact = map (MetaSimplifier.rewrite_rule thms)};
 
 
-(* generalize type/term parameters *)
-
-val maxidx_atts = fold Args.maxidx_values;
-
-fun generalize_facts inner outer facts =
-  let
-    val thy = ProofContext.theory_of inner;
-    val maxidx =
-      fold (fn ((_, atts), bs) => maxidx_atts atts #> fold (maxidx_atts o #2) bs) facts ~1;
-    val exp_fact = map (Thm.adjust_maxidx_thm maxidx) #> Variable.export inner outer;
-    val exp_term = Drule.term_rule thy (singleton exp_fact);
-    val exp_typ = Logic.type_map exp_term;
-    val morphism = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact};
-  in facts_map (morph_ctxt morphism) facts end;
-
-
 (* transfer to theory using closure *)
 
 fun transfer_morphism thy =

--- a/src/Pure/Isar/theory_target.ML	Sat Mar 13 17:05:34 2010 -0800
+++ b/src/Pure/Isar/theory_target.ML	Sat Mar 13 17:36:53 2010 -0800
@@ -179,7 +179,7 @@
   end;
 
 
-(* declare_const *)
+(* consts *)
 
 fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
   if not is_locale then (NoSyn, NoSyn, mx)
@@ -209,34 +209,6 @@
              Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
   end;
 
-fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
-
-fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
-  let
-    val xs = filter depends (#1 (ProofContext.inferred_fixes (Local_Theory.target_of lthy)));
-    val U = map #2 xs ---> T;
-    val (mx1, mx2, mx3) = fork_mixfix ta mx;
-    val (const, lthy') = lthy |>
-      (case Class_Target.instantiation_param lthy b of
-        SOME c' =>
-          if mx3 <> NoSyn then syntax_error c'
-          else Local_Theory.theory_result (AxClass.declare_overloaded (c', U))
-            ##> Class_Target.confirm_declaration b
-        | NONE =>
-            (case Overloading.operation lthy b of
-              SOME (c', _) =>
-                if mx3 <> NoSyn then syntax_error c'
-                else Local_Theory.theory_result (Overloading.declare (c', U))
-                  ##> Overloading.confirm b
-            | NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3))));
-    val t = Term.list_comb (const, map Free xs);
-  in
-    lthy'
-    |> is_locale ? term_syntax ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
-    |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
-    |> Local_Defs.add_def ((b, NoSyn), t)
-  end;
-
 
 (* abbrev *)
 
@@ -271,6 +243,47 @@
 
 (* define *)
 
+local
+
+fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
+
+fun declare_const (ta as Target {target, is_locale, is_class, ...})
+    extra_tfrees xs ((b, T), mx) lthy =
+  let
+    val type_params = map (Logic.mk_type o TFree) extra_tfrees;
+    val term_params =
+      rev (Variable.fixes_of (Local_Theory.target_of lthy))
+      |> map_filter (fn (_, x) =>
+        (case AList.lookup (op =) xs x of
+          SOME T => SOME (Free (x, T))
+        | NONE => NONE));
+    val params = type_params @ term_params;
+
+    val U = map Term.fastype_of params ---> T;
+    val (mx1, mx2, mx3) = fork_mixfix ta mx;
+    val (const, lthy') = lthy |>
+      (case Class_Target.instantiation_param lthy b of
+        SOME c' =>
+          if mx3 <> NoSyn then syntax_error c'
+          else Local_Theory.theory_result (AxClass.declare_overloaded (c', U))
+            ##> Class_Target.confirm_declaration b
+      | NONE =>
+          (case Overloading.operation lthy b of
+            SOME (c', _) =>
+              if mx3 <> NoSyn then syntax_error c'
+              else Local_Theory.theory_result (Overloading.declare (c', U))
+                ##> Overloading.confirm b
+          | NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3))));
+    val t = Term.list_comb (const, params);
+  in
+    lthy'
+    |> is_locale ? term_syntax ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
+    |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
+    |> Local_Defs.add_def ((b, NoSyn), t)
+  end;
+
+in
+
 fun define ta ((b, mx), ((name, atts), rhs)) lthy =
   let
     val thy = ProofContext.theory_of lthy;
@@ -284,20 +297,26 @@
 
     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;
 
     (*const*)
-    val ((lhs, local_def), lthy2) = lthy |> declare_const ta (member (op =) xs) ((b, T), mx);
+    val ((lhs, local_def), lthy2) = lthy |> declare_const ta extra_tfrees xs ((b, T), mx);
     val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
+    val Const (head, _) = Term.head_of lhs';
 
     (*def*)
     val (global_def, lthy3) = lthy2
       |> Local_Theory.theory_result
         (case Overloading.operation lthy b of
-          SOME (_, checked) => Overloading.define checked name' (fst (dest_Const lhs'), rhs')
+          SOME (_, checked) => Overloading.define checked name' (head, rhs')
         | NONE =>
-            if is_none (Class_Target.instantiation_param lthy b)
-            then Thm.add_def false false (name', Logic.mk_equals (lhs', rhs'))
-            else AxClass.define_overloaded name' (fst (dest_Const lhs'), rhs'));
+            if is_some (Class_Target.instantiation_param lthy b)
+            then AxClass.define_overloaded name' (head, rhs')
+            else Thm.add_def false false (name', Logic.mk_equals (lhs', rhs')));
     val def = Local_Defs.trans_terms lthy3
       [(*c == global.c xs*)     local_def,
        (*global.c xs == rhs'*)  global_def,
@@ -308,6 +327,8 @@
       |> notes ta "" [((name', atts), [([def], [])])];
   in ((lhs, (res_name, res)), lthy4) end;
 
+end;
+
 
 (* init various targets *)