typedef etc.: no constraints;

--- a/src/HOL/Import/proof_kernel.ML	Fri Mar 19 00:46:08 2010 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Fri Mar 19 00:47:23 2010 +0100
@@ -2095,7 +2095,7 @@
             val typ = (tycname,tnames,tsyn)
             val ((_, typedef_info), thy') =
               Typedef.add_typedef_global false (SOME (Binding.name thmname))
-                (Binding.name tycname, tnames, tsyn) c NONE (rtac th2 1) thy
+                (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c NONE (rtac th2 1) thy
             val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
 
             val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
@@ -2182,7 +2182,8 @@
             val tsyn = mk_syn thy tycname
             val typ = (tycname,tnames,tsyn)
             val ((_, typedef_info), thy') =
-              Typedef.add_typedef_global false NONE (Binding.name tycname,tnames,tsyn) c
+              Typedef.add_typedef_global false NONE
+                (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c
                 (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy
             val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
             val fulltyname = Sign.intern_type thy' tycname

--- a/src/HOL/Import/replay.ML	Fri Mar 19 00:46:08 2010 +0100
+++ b/src/HOL/Import/replay.ML	Fri Mar 19 00:47:23 2010 +0100
@@ -343,7 +343,8 @@
           | delta (Hol_theorem (thyname, thmname, th)) thy =
             add_hol4_theorem thyname thmname ([], th_of thy th) thy
           | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = 
-            snd (Typedef.add_typedef_global false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
+            snd (Typedef.add_typedef_global false (Option.map Binding.name thmname)
+              (Binding.name t, map (rpair dummyS) vs, mx) c
         (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
           | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
             add_hol4_type_mapping thyname tycname true fulltyname thy

--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Mar 19 00:46:08 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Mar 19 00:47:23 2010 +0100
@@ -616,7 +616,7 @@
       thy4
       |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
           Typedef.add_typedef_global false (SOME (Binding.name name'))
-            (Binding.name name, map fst tvs, mx)
+            (Binding.name name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
             (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
                Const (cname, U --> HOLogic.boolT)) NONE
             (rtac exI 1 THEN rtac CollectI 1 THEN

--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Mar 19 00:46:08 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Mar 19 00:47:23 2010 +0100
@@ -190,7 +190,8 @@
     val (typedefs, thy3) = thy2 |>
       Sign.parent_path |>
       fold_map (fn ((((name, mx), tvs), c), name') =>
-          Typedef.add_typedef_global false (SOME (Binding.name name')) (name, tvs, mx)
+          Typedef.add_typedef_global false (SOME (Binding.name name'))
+            (name, map (rpair dummyS) tvs, mx)
             (Collect $ Const (c, UnivT')) NONE
             (rtac exI 1 THEN rtac CollectI 1 THEN
               QUIET_BREADTH_FIRST (has_fewer_prems 1)

--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Mar 19 00:46:08 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Mar 19 00:47:23 2010 +0100
@@ -82,7 +82,7 @@
 *)
    Local_Theory.theory_result
      (Typedef.add_typedef_global false NONE
-       (qty_name, vs, mx)
+       (qty_name, map (rpair dummyS) vs, mx)
          (typedef_term rel rty lthy)
            NONE typedef_tac) lthy
 end

--- a/src/HOL/Tools/typecopy.ML	Fri Mar 19 00:46:08 2010 +0100
+++ b/src/HOL/Tools/typecopy.ML	Fri Mar 19 00:47:23 2010 +0100
@@ -80,7 +80,8 @@
         end
   in
     thy
-    |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn)
+    |> Typedef.add_typedef_global false (SOME raw_tyco)
+      (raw_tyco, map (fn (v, _) => (v, dummyS)) vs, NoSyn)   (* FIXME keep constraints!? *)
       (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
     |-> (fn (tyco, info) => add_info tyco info)
   end;

--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 19 00:46:08 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 19 00:47:23 2010 +0100
@@ -473,7 +473,7 @@
         val reps = map (mk_Rep_of o tfree) vs;
         val defl = list_ccomb (defl_const, reps);
         val ((_, _, _, {REP, ...}), thy) =
-          Repdef.add_repdef false NONE (tbind, vs, mx) defl NONE thy;
+          Repdef.add_repdef false NONE (tbind, map (rpair dummyS) vs, mx) defl NONE thy;
       in
         (REP, thy)
       end;