explicit ProofContext.check_tfree;

--- a/src/HOL/Tools/typecopy.ML	Thu Apr 15 18:13:25 2010 +0200
+++ b/src/HOL/Tools/typecopy.ML	Thu Apr 15 20:31:21 2010 +0200
@@ -53,8 +53,7 @@
   let
     val ty = Sign.certify_typ thy raw_ty;
     val ctxt = ProofContext.init thy |> Variable.declare_typ ty;
-    val vs = raw_vs |>
-      map (fn (a, S) => (a, if S = dummyS then ProofContext.default_sort ctxt (a, ~1) else S));
+    val vs = map (ProofContext.check_tfree ctxt) raw_vs;
     val tac = Tactic.rtac UNIV_witness 1;
     fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
           Rep_name = c_rep, ...}, { Abs_inject = inject, Abs_inverse = inverse, ... })

--- a/src/Pure/Isar/typedecl.ML	Thu Apr 15 18:13:25 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML	Thu Apr 15 20:31:21 2010 +0200
@@ -45,9 +45,8 @@
     fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b));
 
     val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters";
-    val args = raw_args
-      |> map (fn (a, S) => (a, if S = dummyS then ProofContext.default_sort lthy (a, ~1) else S));
-    val T = Type (Local_Theory.full_name lthy b, map TFree args);
+    val args = map (TFree o ProofContext.check_tfree lthy) raw_args;
+    val T = Type (Local_Theory.full_name lthy b, args);
 
     val bad_args =
       #2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T))