# HG changeset patch
# User wenzelm
# Date 1268949618 -3600
# Node ID 9380fab5f4f7247c1bc0ac1b6949d201e8b2cd77
# Parent  51c6ac100bd9e545d0445c46151a265d62e721d8
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints;

diff -r 51c6ac100bd9 -r 9380fab5f4f7 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Thu Mar 18 22:59:44 2010 +0100
+++ b/src/HOL/Tools/typedef.ML	Thu Mar 18 23:00:18 2010 +0100
@@ -127,8 +127,6 @@
 
 (* prepare_typedef *)
 
-fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
-
 fun prepare_typedef prep_term def_set name (tname, vs, mx) raw_set opt_morphs lthy =
   let
     val full_name = Local_Theory.full_name lthy name;
@@ -137,7 +135,10 @@
 
     (* rhs *)
 
-    val set = prep_term (lthy |> fold declare_type_name vs) raw_set;
+    val (_, tmp_lthy) = lthy |> Typedecl.predeclare_constraints (tname, map (rpair dummyS) vs, mx);
+    val set = prep_term tmp_lthy raw_set;
+    val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set;
+
     val setT = Term.fastype_of set;
     val oldT = HOLogic.dest_setT setT handle TYPE _ =>
       error ("Not a set type: " ^ quote (Syntax.string_of_typ lthy setT));
@@ -148,8 +149,9 @@
 
     (* lhs *)
 
+    val args = map (fn a => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) vs;
     val (newT, typedecl_lthy) = lthy
-      |> Typedecl.typedecl_wrt [set] (tname, vs, mx)
+      |> Typedecl.typedecl (tname, args, mx)
       ||> Variable.declare_term set;
 
     val Type (full_tname, type_args) = newT;