TypeInfer.constrain: canonical argument order;

--- a/src/HOL/Tools/res_reconstruct.ML	Sun Sep 23 22:23:24 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Sun Sep 23 22:23:27 2007 +0200
@@ -238,7 +238,7 @@
   vt0 holds the initial sort constraints, from the conjecture clauses.*)
 fun clause_of_strees ctxt vt0 ts =
   let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in
-    singleton (Syntax.check_terms ctxt) (TypeInfer.constrain (fix_sorts vt dt) HOLogic.boolT)
+    singleton (Syntax.check_terms ctxt) (TypeInfer.constrain HOLogic.boolT (fix_sorts vt dt))
   end;
 
 (*Quantification over a list of Vars. FIXME: for term.ML??*)

--- a/src/HOLCF/Tools/domain/domain_library.ML	Sun Sep 23 22:23:24 2007 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Sun Sep 23 22:23:27 2007 +0200
@@ -153,8 +153,8 @@
 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_constrain      (typ,T) = TypeInfer.constrain T typ;
-fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (mk_lam(x,P)) (typ --> boolT));
+val mk_constrain = uncurry TypeInfer.constrain;
+fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (typ --> boolT) (mk_lam(x,P)));
 end
 
 fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)

--- a/src/HOLCF/Tools/fixrec_package.ML	Sun Sep 23 22:23:24 2007 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML	Sun Sep 23 22:23:27 2007 +0200
@@ -23,7 +23,7 @@
 fun legacy_infer_term thy t =
   singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
 
-fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain t propT);
+fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
 
 
 val fix_eq2 = thm "fix_eq2";

--- a/src/Pure/Syntax/syntax.ML	Sun Sep 23 22:23:24 2007 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Sep 23 22:23:27 2007 +0200
@@ -674,7 +674,7 @@
 
 val check_typs = gen_check fst (op =);
 val check_terms = gen_check snd (op aconv);
-fun check_props ctxt = map (fn t => TypeInfer.constrain t propT) #> check_terms ctxt;
+fun check_props ctxt = map (TypeInfer.constrain propT) #> check_terms ctxt;
 
 val check_typ = singleton o check_typs;
 val check_term = singleton o check_terms;

--- a/src/Pure/Syntax/type_ext.ML	Sun Sep 23 22:23:24 2007 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Sun Sep 23 22:23:27 2007 +0200
@@ -109,10 +109,10 @@
     val decodeT = map_type o typ_of_term (get_sort sort_env) map_sort;
 
     fun decode (Const ("_constrain", _) $ t $ typ) =
-          TypeInfer.constrain (decode t) (decodeT typ)
+          TypeInfer.constrain (decodeT typ) (decode t)
       | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
           if T = dummyT then Abs (x, decodeT typ, decode t)
-          else TypeInfer.constrain (Abs (x, map_type T, decode t)) (decodeT typ --> dummyT)
+          else TypeInfer.constrain (decodeT typ --> dummyT) (Abs (x, map_type T, decode t))
       | decode (Abs (x, T, t)) = Abs (x, map_type T, decode t)
       | decode (t $ u) = decode t $ decode u
       | decode (Const (a, T)) =

--- a/src/Pure/Thy/thy_output.ML	Sun Sep 23 22:23:24 2007 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sun Sep 23 22:23:27 2007 +0200
@@ -434,7 +434,7 @@
   ProofContext.pretty_term_abbrev ctxt o ProofContext.revert_skolems ctxt;
 
 fun pretty_term_typ ctxt t =
-  ProofContext.pretty_term ctxt (TypeInfer.constrain t (Term.fastype_of t));
+  ProofContext.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);
 
 fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of;
 

--- a/src/Pure/Tools/invoke.ML	Sun Sep 23 22:23:24 2007 +0200
+++ b/src/Pure/Tools/invoke.ML	Sun Sep 23 22:23:27 2007 +0200
@@ -100,7 +100,7 @@
 
 fun infer_terms ctxt =
   Syntax.check_terms ctxt o
-    (map (fn (t, T) => TypeInfer.constrain t (TypeInfer.paramify_vars T)));
+    (map (fn (t, T) => TypeInfer.constrain (TypeInfer.paramify_vars T) t));
 
 in
 

--- a/src/Pure/Tools/nbe.ML	Sun Sep 23 22:23:24 2007 +0200
+++ b/src/Pure/Tools/nbe.ML	Sun Sep 23 22:23:27 2007 +0200
@@ -137,7 +137,7 @@
         ^ setmp show_types true (Sign.string_of_term thy) t);
     val ty = type_of t;
     fun constrain t =
-      singleton (Syntax.check_terms (ProofContext.init thy)) (TypeInfer.constrain t ty);
+      singleton (Syntax.check_terms (ProofContext.init thy)) (TypeInfer.constrain ty t);
     val _ = ensure_funs thy funcgr t;
   in
     t

--- a/src/Tools/nbe.ML	Sun Sep 23 22:23:24 2007 +0200
+++ b/src/Tools/nbe.ML	Sun Sep 23 22:23:27 2007 +0200
@@ -327,7 +327,7 @@
       subst_Frees (map (fn (s, T) => (s, Term.Free (s, T))) (Term.add_frees t []))
       #> subst_Vars (map (fn (ixn, T) => (ixn, Var (ixn, T))) (Term.add_vars t []))
     fun constrain t =
-      singleton (Syntax.check_terms (ProofContext.init thy)) (TypeInfer.constrain t ty);
+      singleton (Syntax.check_terms (ProofContext.init thy)) (TypeInfer.constrain ty t);
     fun check_tvars t = if null (Term.term_tvars t) then t else
       error ("Illegal schematic type variables in normalized term: "
         ^ setmp show_types true (Sign.string_of_term thy) t);