# HG changeset patch
# User wenzelm
# Date 1271347762 -7200
# Node ID 1ac501e16a6a9982328b763e799bac8bc79271c5
# Parent  34d1ce2d746d356be3fb871b4626e19a66a85eac
replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
simplified via ProofContext.check_tfree;

diff -r 34d1ce2d746d -r 1ac501e16a6a src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Apr 15 18:00:21 2010 +0200
+++ b/src/HOL/Tools/record.ML	Thu Apr 15 18:09:22 2010 +0200
@@ -2440,15 +2440,14 @@
   end
   handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding));
 
-fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy0 =
+fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy =
   let
-    val thy = Theory.checkpoint thy0;
-    val lthy = Theory_Target.init NONE thy;
-    val params = map (apsnd (Typedecl.read_constraint lthy)) raw_params;
-    val (_, lthy1) = Typedecl.predeclare_constraints (binding, params, NoSyn) lthy;
-    val (parent, lthy2) = read_parent raw_parent lthy1;
-    val (fields, lthy3) = fold_map read_field raw_fields lthy2;
-    val params' = map (fn (a, _) => (a, ProofContext.default_sort lthy3 (a, ~1))) params;
+    val ctxt = ProofContext.init thy;
+    val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
+    val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
+    val (parent, ctxt2) = read_parent raw_parent ctxt1;
+    val (fields, ctxt3) = fold_map read_field raw_fields ctxt2;
+    val params' = map (ProofContext.check_tfree ctxt3) params;
   in thy |> add_record quiet_mode (params', binding) parent fields end;
 
 end;
diff -r 34d1ce2d746d -r 1ac501e16a6a src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Thu Apr 15 18:00:21 2010 +0200
+++ b/src/HOL/Tools/typedef.ML	Thu Apr 15 18:09:22 2010 +0200
@@ -135,9 +135,9 @@
 
     (* rhs *)
 
-    val (_, tmp_lthy) = lthy |> Typedecl.predeclare_constraints (tname, raw_args, mx);
-    val set = prep_term tmp_lthy raw_set;
-    val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set;
+    val tmp_ctxt = lthy |> fold (Variable.declare_typ o TFree) raw_args;
+    val set = prep_term tmp_ctxt raw_set;
+    val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
 
     val setT = Term.fastype_of set;
     val oldT = HOLogic.dest_setT setT handle TYPE _ =>
@@ -149,7 +149,7 @@
 
     (* lhs *)
 
-    val args = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args;
+    val args = map (ProofContext.check_tfree tmp_ctxt') raw_args;
     val (newT, typedecl_lthy) = lthy
       |> Typedecl.typedecl (tname, args, mx)
       ||> Variable.declare_term set;
diff -r 34d1ce2d746d -r 1ac501e16a6a src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Thu Apr 15 18:00:21 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML	Thu Apr 15 18:09:22 2010 +0200
@@ -169,18 +169,18 @@
     val _ = Theory.requires thy "Pcpodef" "pcpodefs";
 
     (*rhs*)
-    val (_, tmp_lthy) =
-      thy |> Theory.copy |> Theory_Target.init NONE
-      |> Typedecl.predeclare_constraints (tname, raw_args, mx);
-    val set = prep_term tmp_lthy raw_set;
-    val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set;
+    val tmp_ctxt =
+      ProofContext.init thy
+      |> fold (Variable.declare_typ o TFree) raw_args;
+    val set = prep_term tmp_ctxt raw_set;
+    val tmp_ctxt' = tmp_ctxt |> Variable.declare_term 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 tmp_lthy setT));
+      error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT));
 
     (*lhs*)
-    val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args;
+    val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args;
     val full_tname = Sign.full_name thy tname;
     val newT = Type (full_tname, map TFree lhs_tfrees);
 
diff -r 34d1ce2d746d -r 1ac501e16a6a src/HOLCF/Tools/repdef.ML
--- a/src/HOLCF/Tools/repdef.ML	Thu Apr 15 18:00:21 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML	Thu Apr 15 18:09:22 2010 +0200
@@ -64,18 +64,18 @@
     val _ = Theory.requires thy "Representable" "repdefs";
 
     (*rhs*)
-    val (_, tmp_lthy) =
-      thy |> Theory.copy |> Theory_Target.init NONE
-      |> Typedecl.predeclare_constraints (tname, raw_args, mx);
-    val defl = prep_term tmp_lthy raw_defl;
-    val tmp_lthy = tmp_lthy |> Variable.declare_constraints defl;
+    val tmp_ctxt =
+      ProofContext.init thy
+      |> fold (Variable.declare_typ o TFree) raw_args;
+    val defl = prep_term tmp_ctxt raw_defl;
+    val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl;
 
     val deflT = Term.fastype_of defl;
     val _ = if deflT = @{typ "udom alg_defl"} then ()
-            else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_lthy deflT));
+            else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT));
 
     (*lhs*)
-    val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy (a, ~1))) raw_args;
+    val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt) raw_args;
     val lhs_sorts = map snd lhs_tfrees;
     val full_tname = Sign.full_name thy tname;
     val newT = Type (full_tname, map TFree lhs_tfrees);
diff -r 34d1ce2d746d -r 1ac501e16a6a src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Thu Apr 15 18:00:21 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML	Thu Apr 15 18:09:22 2010 +0200
@@ -7,8 +7,7 @@
 signature TYPEDECL =
 sig
   val read_constraint: Proof.context -> string option -> sort
-  val predeclare_constraints: binding * (string * sort) list * mixfix ->
-    local_theory -> string * local_theory
+  val basic_typedecl: binding * int * mixfix -> local_theory -> string * local_theory
   val typedecl: binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory
   val typedecl_global: binding * (string * sort) list * mixfix -> theory -> typ * theory
 end;
@@ -16,6 +15,12 @@
 structure Typedecl: TYPEDECL =
 struct
 
+(* constraints *)
+
+fun read_constraint _ NONE = dummyS
+  | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
+
+
 (* primitives *)
 
 fun object_logic_arity name thy =
@@ -33,17 +38,7 @@
   end;
 
 
-(* syntactic version -- useful for internalizing additional types/terms beforehand *)
-
-fun read_constraint _ NONE = dummyS
-  | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
-
-fun predeclare_constraints (b, raw_args, mx) =
-  basic_typedecl (b, length raw_args, mx) ##>
-  fold (Variable.declare_constraints o Logic.mk_type o TFree) raw_args;
-
-
-(* regular version -- without dependencies on type parameters of the context *)
+(* regular typedecl -- without dependencies on type parameters of the context *)
 
 fun typedecl (b, raw_args, mx) lthy =
   let