# HG changeset patch
# User wenzelm
# Date 1284311042 -7200
# Node ID f1ae2493d93ffd02565f6587bcaa213d555f051e
# Parent  d30be67910388c2d99369a18b7c72fb5cdf4944e
eliminated aliases of Type.constraint;

diff -r d30be6791038 -r f1ae2493d93f src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -222,7 +222,7 @@
                 val str =
                   G n Syntax.string_of_term (Config.put show_brackets false ctxt) (term_of ct)
                 val u = Syntax.parse_term ctxt str
-                  |> Type_Infer.constrain T |> Syntax.check_term ctxt
+                  |> Type.constraint T |> Syntax.check_term ctxt
             in
                 if match u
                 then quote str
diff -r d30be6791038 -r f1ae2493d93f src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -879,7 +879,7 @@
     val ranT = range_type fT
 
     val default = Syntax.parse_term lthy default_str
-      |> Type_Infer.constrain fT |> Syntax.check_term lthy
+      |> Type.constraint fT |> Syntax.check_term lthy
 
     val (globals, ctxt') = fix_globals domT ranT fvar lthy
 
diff -r d30be6791038 -r f1ae2493d93f src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -276,7 +276,7 @@
     val lthy1 = Variable.declare_typ rty lthy
     val rel = 
       Syntax.parse_term lthy1 rel_str
-      |> Syntax.type_constraint (rty --> rty --> @{typ bool}) 
+      |> Type.constraint (rty --> rty --> @{typ bool}) 
       |> Syntax.check_term lthy1 
     val lthy2 = Variable.declare_term rel lthy1 
   in
diff -r d30be6791038 -r f1ae2493d93f src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -437,7 +437,7 @@
   in repair_tvar_sorts (do_formula true phi Vartab.empty) end
 
 fun check_formula ctxt =
-  Type_Infer.constrain HOLogic.boolT
+  Type.constraint HOLogic.boolT
   #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
 
 
diff -r d30be6791038 -r f1ae2493d93f src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/HOL/Tools/primrec.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -196,8 +196,7 @@
     val def_name = Thm.def_name (Long_Name.base_name fname);
     val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT])
       (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
-    val rhs = singleton (Syntax.check_terms ctxt)
-      (Type_Infer.constrain varT raw_rhs);
+    val rhs = singleton (Syntax.check_terms ctxt) (Type.constraint varT raw_rhs);
   in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end;
 
 
diff -r d30be6791038 -r f1ae2493d93f src/HOLCF/Tools/Domain/domain_library.ML
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -185,7 +185,7 @@
 fun mk_lam  (x,T) = Abs(x,dummyT,T);
 fun mk_all  (x,P) = HOLogic.mk_all (x,dummyT,P);
 fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
-fun mk_constrainall (x,typ,P) = %%: @{const_name All} $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
+fun mk_constrainall (x,typ,P) = %%: @{const_name All} $ (Type.constraint (typ --> boolT) (mk_lam(x,P)));
 end
 
 fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
diff -r d30be6791038 -r f1ae2493d93f src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -463,7 +463,7 @@
 
   fun legacy_infer_term thy t =
       singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t);
-  fun legacy_infer_prop thy t = legacy_infer_term thy (Type_Infer.constrain propT t);
+  fun legacy_infer_prop thy t = legacy_infer_term thy (Type.constraint propT t);
   fun infer_props thy = map (apsnd (legacy_infer_prop thy));
   fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
   fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
diff -r d30be6791038 -r f1ae2493d93f src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -164,7 +164,7 @@
     (* type inference and contexts *)
     val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
     val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
-    val arg = type_parms @ map2 Type_Infer.constrain parm_types' insts';
+    val arg = type_parms @ map2 Type.constraint parm_types' insts';
     val res = Syntax.check_terms ctxt arg;
     val ctxt' = ctxt |> fold Variable.auto_fixes res;
 
@@ -206,7 +206,7 @@
 
 fun mk_type T = (Logic.mk_type T, []);
 fun mk_term t = (t, []);
-fun mk_propp (p, pats) = (Syntax.type_constraint propT p, pats);
+fun mk_propp (p, pats) = (Type.constraint propT p, pats);
 
 fun dest_type (T, []) = Logic.dest_type T;
 fun dest_term (t, []) = t;
@@ -347,7 +347,7 @@
         val inst' = prep_inst ctxt parm_names inst;
         val parm_types' = map (Type_Infer.paramify_vars o
           Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global) parm_types;
-        val inst'' = map2 Type_Infer.constrain parm_types' inst';
+        val inst'' = map2 Type.constraint parm_types' inst';
         val insts' = insts @ [(loc, (prfx, inst''))];
         val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
         val inst''' = insts'' |> List.last |> snd |> snd;
diff -r d30be6791038 -r f1ae2493d93f src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -763,7 +763,7 @@
       if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
     val (syms, pos) = Syntax.parse_token ctxt markup text;
 
-    fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
+    fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE)
       handle ERROR msg => SOME msg;
     val t =
       Syntax.standard_parse_term check get_sort map_const map_free
@@ -888,7 +888,7 @@
 in
 
 fun read_terms ctxt T =
-  map (Syntax.parse_term ctxt #> Type_Infer.constrain T) #> Syntax.check_terms ctxt;
+  map (Syntax.parse_term ctxt #> Type.constraint T) #> Syntax.check_terms ctxt;
 
 val match_bind = gen_bind read_terms;
 val match_bind_i = gen_bind (fn ctxt => fn _ => map (cert_term ctxt));
diff -r d30be6791038 -r f1ae2493d93f src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -82,7 +82,7 @@
     fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
     val ts = map2 parse Ts ss;
     val ts' =
-      map2 (Type_Infer.constrain o Type_Infer.paramify_vars) Ts ts
+      map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
       |> Syntax.check_terms ((schematic ? ProofContext.set_mode ProofContext.mode_schematic) ctxt)
       |> Variable.polymorphic ctxt;
     val Ts' = map Term.fastype_of ts';
diff -r d30be6791038 -r f1ae2493d93f src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/Pure/Isar/specification.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -102,7 +102,7 @@
     fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
       | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
       | abs_body lev y (t as Free (x, T)) =
-          if x = y then Type_Infer.constrain (uniform_typing x) (Type_Infer.constrain T (Bound lev))
+          if x = y then Type.constraint (uniform_typing x) (Type.constraint T (Bound lev))
           else t
       | abs_body _ _ a = a;
     fun close (y, U) B =
diff -r d30be6791038 -r f1ae2493d93f src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/Pure/Proof/extraction.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -164,7 +164,7 @@
       |> Proof_Syntax.strip_sorts_consttypes
       |> ProofContext.set_defsort [];
     val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
-  in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
+  in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
 
 
 (**** theory data ****)
diff -r d30be6791038 -r f1ae2493d93f src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -223,7 +223,7 @@
   in
     fn ty => fn s =>
       (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
-      |> Type_Infer.constrain ty |> Syntax.check_term ctxt
+      |> Type.constraint ty |> Syntax.check_term ctxt
   end;
 
 fun read_proof thy topsort =
diff -r d30be6791038 -r f1ae2493d93f src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -286,7 +286,7 @@
 
 val check_typs = gen_check fst false;
 val check_terms = gen_check snd false;
-fun check_props ctxt = map (Type_Ext.type_constraint propT) #> check_terms ctxt;
+fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
 
 val check_typ = singleton o check_typs;
 val check_term = singleton o check_terms;
diff -r d30be6791038 -r f1ae2493d93f src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -9,7 +9,6 @@
   val sort_of_term: term -> sort
   val term_sorts: term -> (indexname * sort) list
   val typ_of_term: (indexname -> sort) -> term -> typ
-  val type_constraint: typ -> term -> term
   val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
     (string -> bool * string) -> (string -> string option) -> term -> term
   val term_of_typ: bool -> typ -> term
@@ -104,19 +103,15 @@
 
 (* decode_term -- transform parse tree into raw term *)
 
-fun type_constraint T t =
-  if T = dummyT then t
-  else Const ("_type_constraint_", T --> T) $ t;
-
 fun decode_term get_sort map_const map_free tm =
   let
     val decodeT = typ_of_term (get_sort (term_sorts tm));
 
     fun decode (Const ("_constrain", _) $ t $ typ) =
-          type_constraint (decodeT typ) (decode t)
+          Type.constraint (decodeT typ) (decode t)
       | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
           if T = dummyT then Abs (x, decodeT typ, decode t)
-          else type_constraint (decodeT typ --> dummyT) (Abs (x, T, decode t))
+          else Type.constraint (decodeT typ --> dummyT) (Abs (x, T, decode t))
       | decode (Abs (x, T, t)) = Abs (x, T, decode t)
       | decode (t $ u) = decode t $ decode u
       | decode (Const (a, T)) =
diff -r d30be6791038 -r f1ae2493d93f src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -482,7 +482,7 @@
 
 fun pretty_term_typ ctxt (style, t) =
   let val t' = style t
-  in pretty_term ctxt (Type_Infer.constrain (Term.fastype_of t') t') end;
+  in pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end;
 
 fun pretty_term_typeof ctxt (style, t) =
   Syntax.pretty_typ ctxt (Term.fastype_of (style t));
diff -r d30be6791038 -r f1ae2493d93f src/Pure/type.ML
--- a/src/Pure/type.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/Pure/type.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -7,6 +7,8 @@
 
 signature TYPE =
 sig
+  (*constraints*)
+  val constraint: typ -> term -> term
   (*type signatures and certified types*)
   datatype decl =
     LogicalType of int |
@@ -96,6 +98,14 @@
 structure Type: TYPE =
 struct
 
+(** constraints **)
+
+fun constraint T t =
+  if T = dummyT then t
+  else Const ("_type_constraint_", T --> T) $ t;
+
+
+
 (** type signatures and certified types **)
 
 (* type declarations *)
diff -r d30be6791038 -r f1ae2493d93f src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/Pure/type_infer.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -8,7 +8,6 @@
 sig
   val anyT: sort -> typ
   val polymorphicT: typ -> typ
-  val constrain: typ -> term -> term
   val is_param: indexname -> bool
   val param: int -> string * sort -> typ
   val paramify_vars: typ -> typ
@@ -31,8 +30,6 @@
 (*indicate polymorphic Vars*)
 fun polymorphicT T = Type ("_polymorphic_", [T]);
 
-val constrain = Syntax.type_constraint;
-
 
 (* type inference parameters -- may get instantiated *)
 
@@ -418,8 +415,8 @@
     (*constrain vars*)
     val get_type = the_default dummyT o var_type;
     val constrain_vars = Term.map_aterms
-      (fn Free (x, T) => constrain T (Free (x, get_type (x, ~1)))
-        | Var (xi, T) => constrain T (Var (xi, get_type xi))
+      (fn Free (x, T) => Type.constraint T (Free (x, get_type (x, ~1)))
+        | Var (xi, T) => Type.constraint T (Var (xi, get_type xi))
         | t => t);
 
     (*convert to preterms*)
diff -r d30be6791038 -r f1ae2493d93f src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/Tools/misc_legacy.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -30,7 +30,7 @@
       |> ProofContext.allow_dummies
       |> ProofContext.set_mode ProofContext.mode_schematic;
     val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
-  in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
+  in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
 
 
 (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
diff -r d30be6791038 -r f1ae2493d93f src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/Tools/nbe.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -551,7 +551,7 @@
     fun type_infer t =
       singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
         (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
-      (Type_Infer.constrain ty' t);
+      (Type.constraint ty' t);
     val string_of_term =
       Syntax.string_of_term (Config.put show_types true (Syntax.init_pretty_global thy));
     fun check_tvars t =
diff -r d30be6791038 -r f1ae2493d93f src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -403,7 +403,7 @@
   let
     val ctxt = ProofContext.init_global thy;
     fun read_is strs =
-      map (Syntax.parse_term ctxt #> Type_Infer.constrain @{typ i}) strs
+      map (Syntax.parse_term ctxt #> Type.constraint @{typ i}) strs
       |> Syntax.check_terms ctxt;
 
     val rec_tms = read_is srec_tms;
diff -r d30be6791038 -r f1ae2493d93f src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -555,7 +555,7 @@
     (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
   let
     val ctxt = ProofContext.init_global thy;
-    val read_terms = map (Syntax.parse_term ctxt #> Type_Infer.constrain Ind_Syntax.iT)
+    val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT)
       #> Syntax.check_terms ctxt;
 
     val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;
diff -r d30be6791038 -r f1ae2493d93f src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/ZF/ind_syntax.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -66,7 +66,7 @@
 
 (*read a constructor specification*)
 fun read_construct ctxt (id: string, sprems, syn: mixfix) =
-    let val prems = map (Syntax.parse_term ctxt #> Type_Infer.constrain FOLogic.oT) sprems
+    let val prems = map (Syntax.parse_term ctxt #> Type.constraint FOLogic.oT) sprems
           |> Syntax.check_terms ctxt
         val args = map (#1 o dest_mem) prems
         val T = (map (#2 o dest_Free) args) ---> iT