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