# HG changeset patch
# User wenzelm
# Date 1268508862 -3600
# Node ID eafaa999071260ea3f4cb6ecd52288322eac124a
# Parent  09e238561460a88c6cbf0200380ee0436574feae
Local_Theory.define handles hidden polymorphism;

diff -r 09e238561460 -r eafaa9990712 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Sat Mar 13 20:33:14 2010 +0100
+++ b/src/HOL/Tools/typedef.ML	Sat Mar 13 20:34:22 2010 +0100
@@ -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);