# HG changeset patch
# User wenzelm
# Date 1271343349 -7200
# Node ID 123f721c9a377fa9b909e23eb86a2eebf52c9d40
# Parent  5ca66e58dcfa714ea33a4b7ec8be79a9ce54b35d
typecopy: observe given sort constraints more precisely;

diff -r 5ca66e58dcfa -r 123f721c9a37 src/HOL/Tools/typecopy.ML
--- a/src/HOL/Tools/typecopy.ML	Thu Apr 15 15:39:50 2010 +0200
+++ b/src/HOL/Tools/typecopy.ML	Thu Apr 15 16:55:49 2010 +0200
@@ -8,7 +8,7 @@
 sig
   type info = { vs: (string * sort) list, constr: string, typ: typ,
     inject: thm, proj: string * typ, proj_def: thm }
-  val typecopy: binding * string list -> typ -> (binding * binding) option
+  val typecopy: binding * (string * sort) list -> typ -> (binding * binding) option
     -> theory -> (string * info) * theory
   val get_info: theory -> string -> info option
   val interpretation: (string -> theory -> theory) -> theory -> theory
@@ -52,8 +52,9 @@
 fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
   let
     val ty = Sign.certify_typ thy raw_ty;
-    val vs =
-      AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT ty [])) raw_vs;
+    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 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, ... })
@@ -80,8 +81,7 @@
         end
   in
     thy
-    |> Typedef.add_typedef_global false (SOME raw_tyco)
-      (raw_tyco, map (fn (v, _) => (v, dummyS)) vs, NoSyn)   (* FIXME keep constraints!? *)
+    |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
       (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
     |-> (fn (tyco, info) => add_info tyco info)
   end;