# 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);