# HG changeset patch
# User wenzelm
# Date 1284377624 -7200
# Node ID 2f38fa28e124f772ed40d4aef381271e1c41fa2c
# Parent  f9371c0751f5c655d61a126f446908b90df14d0a# Parent  e275d581a2181aa30172dc09f61a9fe26d37380c
merged

diff -r f9371c0751f5 -r 2f38fa28e124 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/HOL/Tools/primrec.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/HOLCF/Tools/Domain/domain_library.ML
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Sep 13 13:33:44 2010 +0200
@@ -599,7 +599,7 @@
 
 fun prepare_patterns ctxt =
   let val Mode {pattern, ...} = get_mode ctxt in
-    Type_Infer.fixate_params (Variable.names_of ctxt) #>
+    Type_Infer.fixate ctxt #>
     pattern ? Variable.polymorphic ctxt #>
     (map o Term.map_types) (prepare_patternT ctxt) #>
     (if pattern then prepare_dummies else map (check_dummies ctxt))
@@ -698,11 +698,8 @@
   let val Mode {pattern, ...} = get_mode ctxt
   in Variable.def_type ctxt pattern end;
 
-fun standard_infer_types ctxt ts =
-  Type_Infer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
-    (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt)
-    (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
-  handle TYPE (msg, _, _) => error msg;
+fun standard_infer_types ctxt =
+  Type_Infer.infer_types ctxt (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt);
 
 local
 
@@ -763,7 +760,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 +885,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 f9371c0751f5 -r 2f38fa28e124 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/Isar/proof_display.ML	Mon Sep 13 13:33:44 2010 +0200
@@ -93,7 +93,7 @@
 fun print_results do_print ctxt ((kind, name), facts) =
   if not do_print orelse kind = "" then ()
   else if name = "" then
-    Pretty.writeln (Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
+    Pretty.writeln (Pretty.block (Pretty.command kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
   else Pretty.writeln
     (case facts of
       [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
diff -r f9371c0751f5 -r 2f38fa28e124 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/Isar/runtime.ML	Mon Sep 13 13:33:44 2010 +0200
@@ -34,7 +34,7 @@
 exception CONTEXT of Proof.context * exn;
 
 fun exn_context NONE exn = exn
-  | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn);
+  | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);
 
 
 (* exn_message *)
diff -r f9371c0751f5 -r 2f38fa28e124 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/Isar/specification.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Sep 13 13:33:44 2010 +0200
@@ -619,7 +619,8 @@
 fun command tr st =
   (case transition (! interact) tr st of
     SOME (st', NONE) => st'
-  | SOME (_, SOME exn_info) => raise Runtime.EXCURSION_FAIL exn_info
+  | SOME (_, SOME (exn, info)) =>
+      if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
   | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
 
 fun command_result tr st =
diff -r f9371c0751f5 -r 2f38fa28e124 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/Proof/extraction.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/ROOT.ML	Mon Sep 13 13:33:44 2010 +0200
@@ -116,8 +116,6 @@
 use "Syntax/printer.ML";
 use "Syntax/syntax.ML";
 
-use "type_infer.ML";
-
 
 (* core of tactical proof system *)
 
@@ -159,6 +157,7 @@
 use "Isar/rule_cases.ML";
 use "Isar/auto_bind.ML";
 use "Isar/local_syntax.ML";
+use "type_infer.ML";
 use "Isar/proof_context.ML";
 use "Isar/local_defs.ML";
 
diff -r f9371c0751f5 -r 2f38fa28e124 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/sign.ML	Mon Sep 13 13:33:44 2010 +0200
@@ -29,6 +29,7 @@
   val defaultS: theory -> sort
   val subsort: theory -> sort * sort -> bool
   val of_sort: theory -> typ * sort -> bool
+  val inter_sort: theory -> sort * sort -> sort
   val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list
   val is_logtype: theory -> string -> bool
   val typ_instance: theory -> typ * typ -> bool
@@ -201,6 +202,7 @@
 val defaultS = Type.defaultS o tsig_of;
 val subsort = Type.subsort o tsig_of;
 val of_sort = Type.of_sort o tsig_of;
+val inter_sort = Type.inter_sort o tsig_of;
 val witness_sorts = Type.witness_sorts o tsig_of;
 val is_logtype = member (op =) o Type.logical_types o tsig_of;
 
@@ -265,12 +267,12 @@
 
 fun type_check pp tm =
   let
-    fun err_appl why bs t T u U =
+    fun err_appl bs t T u U =
       let
         val xs = map Free bs;           (*we do not rename here*)
         val t' = subst_bounds (xs, t);
         val u' = subst_bounds (xs, u);
-        val msg = cat_lines (Type_Infer.appl_error pp why t' T u' U);
+        val msg = Type.appl_error pp t' T u' U;
       in raise TYPE (msg, [T, U], [t', u']) end;
 
     fun typ_of (_, Const (_, T)) = T
@@ -283,8 +285,8 @@
           let val T = typ_of (bs, t) and U = typ_of (bs, u) in
             (case T of
               Type ("fun", [T1, T2]) =>
-                if T1 = U then T2 else err_appl "Incompatible operand type" bs t T u U
-            | _ => err_appl "Operator not of function type" bs t T u U)
+                if T1 = U then T2 else err_appl bs t T u U
+            | _ => err_appl bs t T u U)
           end;
   in typ_of ([], tm) end;
 
diff -r f9371c0751f5 -r 2f38fa28e124 src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/term.ML	Mon Sep 13 13:33:44 2010 +0200
@@ -420,7 +420,7 @@
     fun map_aux (Const (a, T)) = Const (a, f T)
       | map_aux (Free (a, T)) = Free (a, f T)
       | map_aux (Var (v, T)) = Var (v, f T)
-      | map_aux (t as Bound _)  = t
+      | map_aux (Bound i) = Bound i
       | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
       | map_aux (t $ u) = map_aux t $ map_aux u;
   in map_aux end;
diff -r f9371c0751f5 -r 2f38fa28e124 src/Pure/type.ML
--- a/src/Pure/type.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/type.ML	Mon Sep 13 13:33:44 2010 +0200
@@ -7,6 +7,11 @@
 
 signature TYPE =
 sig
+  (*constraints*)
+  val mark_polymorphic: typ -> typ
+  val constraint: typ -> term -> term
+  val strip_constraints: term -> term
+  val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string
   (*type signatures and certified types*)
   datatype decl =
     LogicalType of int |
@@ -96,6 +101,44 @@
 structure Type: TYPE =
 struct
 
+(** constraints **)
+
+(*indicate polymorphic Vars*)
+fun mark_polymorphic T = Type ("_polymorphic_", [T]);
+
+fun constraint T t =
+  if T = dummyT then t
+  else Const ("_type_constraint_", T --> T) $ t;
+
+fun strip_constraints (Const ("_type_constraint_", _) $ t) = strip_constraints t
+  | strip_constraints (t $ u) = strip_constraints t $ strip_constraints u
+  | strip_constraints (Abs (x, T, t)) = Abs (x, T, strip_constraints t)
+  | strip_constraints a = a;
+
+fun appl_error pp (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
+      cat_lines
+       ["Failed to meet type constraint:", "",
+        Pretty.string_of (Pretty.block
+         [Pretty.str "Term:", Pretty.brk 2, Pretty.term pp u,
+          Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]),
+        Pretty.string_of (Pretty.block
+         [Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp T])]
+  | appl_error pp t T u U =
+      cat_lines
+       ["Type error in application: " ^
+          (case T of
+            Type ("fun", _) => "incompatible operand type"
+          | _ => "operator not of function type"),
+        "",
+        Pretty.string_of (Pretty.block
+          [Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t,
+            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]),
+        Pretty.string_of (Pretty.block
+          [Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u,
+            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U])];
+
+
+
 (** type signatures and certified types **)
 
 (* type declarations *)
diff -r f9371c0751f5 -r 2f38fa28e124 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/type_infer.ML	Mon Sep 13 13:33:44 2010 +0200
@@ -1,44 +1,47 @@
 (*  Title:      Pure/type_infer.ML
     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
 
-Simple type inference.
+Representation of type-inference problems.  Simple type inference.
 *)
 
 signature TYPE_INFER =
 sig
+  val is_param: indexname -> bool
+  val is_paramT: typ -> bool
+  val param: int -> string * sort -> typ
   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
   val paramify_dummies: typ -> int -> typ * int
-  val fixate_params: Name.context -> term list -> term list
-  val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
-  val infer_types: Pretty.pp -> Type.tsig -> (typ list -> typ list) ->
-    (string -> typ option) -> (indexname -> typ option) -> Name.context -> int ->
+  val deref: typ Vartab.table -> typ -> typ
+  val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
+  val fixate: Proof.context -> term list -> term list
+  val prepare: Proof.context -> (string -> typ option) -> (string * int -> typ option) ->
+    term list -> int * term list
+  val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
     term list -> term list
 end;
 
 structure Type_Infer: TYPE_INFER =
 struct
 
+(** type parameters and constraints **)
 
-(** type parameters and constraints **)
+(* type inference parameters -- may get instantiated *)
+
+fun is_param (x, _: int) = String.isPrefix "?" x;
+
+fun is_paramT (TVar (xi, _)) = is_param xi
+  | is_paramT _ = false;
+
+fun param i (x, S) = TVar (("?" ^ x, i), S);
+
+fun mk_param i S = TVar (("?'a", i), S);
+
+
+(* pre-stage parameters *)
 
 fun anyT S = TFree ("'_dummy_", S);
 
-(*indicate polymorphic Vars*)
-fun polymorphicT T = Type ("_polymorphic_", [T]);
-
-val constrain = Syntax.type_constraint;
-
-
-(* user parameters *)
-
-fun is_param (x, _: int) = String.isPrefix "?" x;
-fun param i (x, S) = TVar (("?" ^ x, i), S);
-
 val paramify_vars =
   Same.commit
     (Term_Subst.map_atypsT_same
@@ -56,94 +59,44 @@
       | paramify T maxidx = (T, maxidx);
   in paramify end;
 
-fun fixate_params name_context ts =
-  let
-    fun subst_param (xi, S) (inst, used) =
-      if is_param xi then
-        let
-          val [a] = Name.invents used Name.aT 1;
-          val used' = Name.declare a used;
-        in (((xi, S), TFree (a, S)) :: inst, used') end
-      else (inst, used);
-    val name_context' = (fold o fold_types) Term.declare_typ_names ts name_context;
-    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], name_context');
-  in (map o map_types) (Term_Subst.instantiateT inst) ts end;
-
 
 
-(** pretyps and preterms **)
-
-(*parameters may get instantiated, anything else is rigid*)
-datatype pretyp =
-  PType of string * pretyp list |
-  PTFree of string * sort |
-  PTVar of indexname * sort |
-  Param of int * sort;
-
-datatype preterm =
-  PConst of string * pretyp |
-  PFree of string * pretyp |
-  PVar of indexname * pretyp |
-  PBound of int |
-  PAbs of string * pretyp * preterm |
-  PAppl of preterm * preterm |
-  Constraint of preterm * pretyp;
-
-
-(* utils *)
+(** prepare types/terms: create inference parameters **)
 
-fun deref tye (T as Param (i, S)) =
-      (case Inttab.lookup tye i of
-        NONE => T
-      | SOME U => deref tye U)
-  | deref tye T = T;
+(* prepare_typ *)
 
-fun fold_pretyps f (PConst (_, T)) x = f T x
-  | fold_pretyps f (PFree (_, T)) x = f T x
-  | fold_pretyps f (PVar (_, T)) x = f T x
-  | fold_pretyps _ (PBound _) x = x
-  | fold_pretyps f (PAbs (_, T, t)) x = fold_pretyps f t (f T x)
-  | fold_pretyps f (PAppl (t, u)) x = fold_pretyps f u (fold_pretyps f t x)
-  | fold_pretyps f (Constraint (t, T)) x = f T (fold_pretyps f t x);
-
-
-
-(** raw typs/terms to pretyps/preterms **)
-
-(* pretyp_of *)
-
-fun pretyp_of is_para typ params_idx =
+fun prepare_typ typ params_idx =
   let
     val (params', idx) = fold_atyps
       (fn TVar (xi as (x, _), S) =>
           (fn ps_idx as (ps, idx) =>
-            if is_para xi andalso not (Vartab.defined ps xi)
-            then (Vartab.update (xi, Param (idx, S)) ps, idx + 1) else ps_idx)
+            if is_param xi andalso not (Vartab.defined ps xi)
+            then (Vartab.update (xi, mk_param idx S) ps, idx + 1) else ps_idx)
         | _ => I) typ params_idx;
 
-    fun pre_of (TVar (v as (xi, _))) idx =
+    fun prepare (T as Type (a, Ts)) idx =
+          if T = dummyT then (mk_param idx [], idx + 1)
+          else
+            let val (Ts', idx') = fold_map prepare Ts idx
+            in (Type (a, Ts'), idx') end
+      | prepare (T as TVar (xi, _)) idx =
           (case Vartab.lookup params' xi of
-            NONE => PTVar v
+            NONE => T
           | SOME p => p, idx)
-      | pre_of (TFree ("'_dummy_", S)) idx = (Param (idx, S), idx + 1)
-      | pre_of (TFree v) idx = (PTFree v, idx)
-      | pre_of (T as Type (a, Ts)) idx =
-          if T = dummyT then (Param (idx, []), idx + 1)
-          else
-            let val (Ts', idx') = fold_map pre_of Ts idx
-            in (PType (a, Ts'), idx') end;
+      | prepare (TFree ("'_dummy_", S)) idx = (mk_param idx S, idx + 1)
+      | prepare (T as TFree _) idx = (T, idx);
 
-    val (ptyp, idx') = pre_of typ idx;
-  in (ptyp, (params', idx')) end;
+    val (typ', idx') = prepare typ idx;
+  in (typ', (params', idx')) end;
 
 
-(* preterm_of *)
+(* prepare_term *)
 
-fun preterm_of const_type is_para tm (vparams, params, idx) =
+fun prepare_term const_type tm (vparams, params, idx) =
   let
     fun add_vparm xi (ps_idx as (ps, idx)) =
       if not (Vartab.defined ps xi) then
-        (Vartab.update (xi, Param (idx, [])) ps, idx + 1)
+        (Vartab.update (xi, mk_param idx []) ps, idx + 1)
       else ps_idx;
 
     val (vparams', idx') = fold_aterms
@@ -154,130 +107,134 @@
       tm (vparams, idx);
     fun var_param xi = the (Vartab.lookup vparams' xi);
 
-    val preT_of = pretyp_of is_para;
-    fun polyT_of T idx = apsnd snd (pretyp_of (K true) T (Vartab.empty, idx));
+    fun polyT_of T idx = apsnd snd (prepare_typ (paramify_vars T) (Vartab.empty, idx));
 
     fun constraint T t ps =
       if T = dummyT then (t, ps)
       else
-        let val (T', ps') = preT_of T ps
-        in (Constraint (t, T'), ps') end;
+        let val (T', ps') = prepare_typ T ps
+        in (Type.constraint T' t, ps') end;
 
-    fun pre_of (Const (c, T)) (ps, idx) =
+    fun prepare (Const ("_type_constraint_", T) $ t) ps_idx =
+          let
+            val (T', ps_idx') = prepare_typ T ps_idx;
+            val (t', ps_idx'') = prepare t ps_idx';
+          in (Const ("_type_constraint_", T') $ t', ps_idx'') end
+      | prepare (Const (c, T)) (ps, idx) =
           (case const_type c of
             SOME U =>
-              let val (pU, idx') = polyT_of U idx
-              in constraint T (PConst (c, pU)) (ps, idx') end
-          | NONE => raise TYPE ("No such constant: " ^ quote c, [], []))
-      | pre_of (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
-          let val (pT, idx') = polyT_of T idx
-          in (PVar (xi, pT), (ps, idx')) end
-      | pre_of (Var (xi, T)) ps_idx = constraint T (PVar (xi, var_param xi)) ps_idx
-      | pre_of (Free (x, T)) ps_idx = constraint T (PFree (x, var_param (x, ~1))) ps_idx
-      | pre_of (Const ("_type_constraint_", Type ("fun", [T, _])) $ t) ps_idx =
-          pre_of t ps_idx |-> constraint T
-      | pre_of (Bound i) ps_idx = (PBound i, ps_idx)
-      | pre_of (Abs (x, T, t)) ps_idx =
+              let val (U', idx') = polyT_of U idx
+              in constraint T (Const (c, U')) (ps, idx') end
+          | NONE => error ("Undeclared constant: " ^ quote c))
+      | prepare (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
+          let val (T', idx') = polyT_of T idx
+          in (Var (xi, T'), (ps, idx')) end
+      | prepare (Var (xi, T)) ps_idx = constraint T (Var (xi, var_param xi)) ps_idx
+      | prepare (Free (x, T)) ps_idx = constraint T (Free (x, var_param (x, ~1))) ps_idx
+      | prepare (Bound i) ps_idx = (Bound i, ps_idx)
+      | prepare (Abs (x, T, t)) ps_idx =
           let
-            val (T', ps_idx') = preT_of T ps_idx;
-            val (t', ps_idx'') = pre_of t ps_idx';
-          in (PAbs (x, T', t'), ps_idx'') end
-      | pre_of (t $ u) ps_idx =
+            val (T', ps_idx') = prepare_typ T ps_idx;
+            val (t', ps_idx'') = prepare t ps_idx';
+          in (Abs (x, T', t'), ps_idx'') end
+      | prepare (t $ u) ps_idx =
           let
-            val (t', ps_idx') = pre_of t ps_idx;
-            val (u', ps_idx'') = pre_of u ps_idx';
-          in (PAppl (t', u'), ps_idx'') end;
+            val (t', ps_idx') = prepare t ps_idx;
+            val (u', ps_idx'') = prepare u ps_idx';
+          in (t' $ u', ps_idx'') end;
 
-    val (tm', (params', idx'')) = pre_of tm (params, idx');
+    val (tm', (params', idx'')) = prepare tm (params, idx');
   in (tm', (vparams', params', idx'')) end;
 
 
 
-(** pretyps/terms to typs/terms **)
+(** results **)
 
-(* add_parms *)
+(* dereferenced views *)
 
-fun add_parmsT tye T =
+fun deref tye (T as TVar (xi, _)) =
+      (case Vartab.lookup tye xi of
+        NONE => T
+      | SOME U => deref tye U)
+  | deref tye T = T;
+
+fun add_parms tye T =
   (case deref tye T of
-    PType (_, Ts) => fold (add_parmsT tye) Ts
-  | Param (i, _) => insert (op =) i
+    Type (_, Ts) => fold (add_parms tye) Ts
+  | TVar (xi, _) => if is_param xi then insert (op =) xi else I
   | _ => I);
 
-fun add_parms tye = fold_pretyps (add_parmsT tye);
-
-
-(* add_names *)
-
-fun add_namesT tye T =
+fun add_names tye T =
   (case deref tye T of
-    PType (_, Ts) => fold (add_namesT tye) Ts
-  | PTFree (x, _) => Name.declare x
-  | PTVar ((x, _), _) => Name.declare x
-  | Param _ => I);
-
-fun add_names tye = fold_pretyps (add_namesT tye);
+    Type (_, Ts) => fold (add_names tye) Ts
+  | TFree (x, _) => Name.declare x
+  | TVar ((x, i), _) => if is_param (x, i) then I else Name.declare x);
 
 
-(* simple_typ/term_of *)
+(* finish -- standardize remaining parameters *)
 
-fun simple_typ_of tye f T =
-  (case deref tye T of
-    PType (a, Ts) => Type (a, map (simple_typ_of tye f) Ts)
-  | PTFree v => TFree v
-  | PTVar v => TVar v
-  | Param (i, S) => TVar (f i, S));
+fun finish ctxt tye (Ts, ts) =
+  let
+    val used =
+      (fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt));
+    val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
+    val names = Name.invents used ("?" ^ Name.aT) (length parms);
+    val tab = Vartab.make (parms ~~ names);
 
-(*convert types, drop constraints*)
-fun simple_term_of tye f (PConst (c, T)) = Const (c, simple_typ_of tye f T)
-  | simple_term_of tye f (PFree (x, T)) = Free (x, simple_typ_of tye f T)
-  | simple_term_of tye f (PVar (xi, T)) = Var (xi, simple_typ_of tye f T)
-  | simple_term_of tye f (PBound i) = Bound i
-  | simple_term_of tye f (PAbs (x, T, t)) =
-      Abs (x, simple_typ_of tye f T, simple_term_of tye f t)
-  | simple_term_of tye f (PAppl (t, u)) =
-      simple_term_of tye f t $ simple_term_of tye f u
-  | simple_term_of tye f (Constraint (t, _)) = simple_term_of tye f t;
+    fun finish_typ T =
+      (case deref tye T of
+        Type (a, Ts) => Type (a, map finish_typ Ts)
+      | U as TFree _ => U
+      | U as TVar (xi, S) =>
+          (case Vartab.lookup tab xi of
+            NONE => U
+          | SOME a => TVar ((a, 0), S)));
+  in (map finish_typ Ts, map (Type.strip_constraints o Term.map_types finish_typ) ts) end;
 
 
-(* typs_terms_of *)
+(* fixate -- introduce fresh type variables *)
 
-fun typs_terms_of tye used maxidx (Ts, ts) =
+fun fixate ctxt ts =
   let
-    val used' = fold (add_names tye) ts (fold (add_namesT tye) Ts used);
-    val parms = rev (fold (add_parms tye) ts (fold (add_parmsT tye) Ts []));
-    val names = Name.invents used' ("?" ^ Name.aT) (length parms);
-    val tab = Inttab.make (parms ~~ names);
-    fun f i = (the (Inttab.lookup tab i), maxidx + 1);
-  in (map (simple_typ_of tye f) Ts, map (simple_term_of tye f) ts) end;
+    fun subst_param (xi, S) (inst, used) =
+      if is_param xi then
+        let
+          val [a] = Name.invents used Name.aT 1;
+          val used' = Name.declare a used;
+        in (((xi, S), TFree (a, S)) :: inst, used') end
+      else (inst, used);
+    val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
+    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
+  in (map o map_types) (Term_Subst.instantiateT inst) ts end;
 
 
 
 (** order-sorted unification of types **)
 
-exception NO_UNIFIER of string * pretyp Inttab.table;
+exception NO_UNIFIER of string * typ Vartab.table;
 
-fun unify pp tsig =
+fun unify ctxt pp =
   let
+    val thy = ProofContext.theory_of ctxt;
+    val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
+
 
     (* adjust sorts of parameters *)
 
     fun not_of_sort x S' S =
-      "Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^
-        Pretty.string_of_sort pp S;
+      "Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^
+        Syntax.string_of_sort ctxt S;
 
     fun meet (_, []) tye_idx = tye_idx
-      | meet (Param (i, S'), S) (tye_idx as (tye, idx)) =
-          if Type.subsort tsig (S', S) then tye_idx
-          else (Inttab.update_new (i,
-            Param (idx, Type.inter_sort tsig (S', S))) tye, idx + 1)
-      | meet (PType (a, Ts), S) (tye_idx as (tye, _)) =
-          meets (Ts, Type.arity_sorts pp tsig a S
-            handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
-      | meet (PTFree (x, S'), S) (tye_idx as (tye, _)) =
-          if Type.subsort tsig (S', S) then tye_idx
+      | meet (Type (a, Ts), S) (tye_idx as (tye, _)) =
+          meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
+      | meet (TFree (x, S'), S) (tye_idx as (tye, _)) =
+          if Sign.subsort thy (S', S) then tye_idx
           else raise NO_UNIFIER (not_of_sort x S' S, tye)
-      | meet (PTVar (xi, S'), S) (tye_idx as (tye, _)) =
-          if Type.subsort tsig (S', S) then tye_idx
+      | meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) =
+          if Sign.subsort thy (S', S) then tye_idx
+          else if is_param xi then
+            (Vartab.update_new (xi, mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1)
           else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye)
     and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) =
           meets (Ts, Ss) (meet (deref tye T, S) tye_idx)
@@ -286,149 +243,115 @@
 
     (* occurs check and assignment *)
 
-    fun occurs_check tye i (Param (i', S)) =
-          if i = i' then raise NO_UNIFIER ("Occurs check!", tye)
+    fun occurs_check tye xi (TVar (xi', S)) =
+          if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye)
           else
-            (case Inttab.lookup tye i' of
+            (case Vartab.lookup tye xi' of
               NONE => ()
-            | SOME T => occurs_check tye i T)
-      | occurs_check tye i (PType (_, Ts)) = List.app (occurs_check tye i) Ts
+            | SOME T => occurs_check tye xi T)
+      | occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts
       | occurs_check _ _ _ = ();
 
-    fun assign i (T as Param (i', _)) S tye_idx =
-          if i = i' then tye_idx
-          else tye_idx |> meet (T, S) |>> Inttab.update_new (i, T)
-      | assign i T S (tye_idx as (tye, _)) =
-          (occurs_check tye i T; tye_idx |> meet (T, S) |>> Inttab.update_new (i, T));
+    fun assign xi (T as TVar (xi', _)) S env =
+          if xi = xi' then env
+          else env |> meet (T, S) |>> Vartab.update_new (xi, T)
+      | assign xi T S (env as (tye, _)) =
+          (occurs_check tye xi T; env |> meet (T, S) |>> Vartab.update_new (xi, T));
 
 
     (* unification *)
 
-    fun unif (T1, T2) (tye_idx as (tye, idx)) =
-      (case (deref tye T1, deref tye T2) of
-        (Param (i, S), T) => assign i T S tye_idx
-      | (T, Param (i, S)) => assign i T S tye_idx
-      | (PType (a, Ts), PType (b, Us)) =>
+    fun show_tycon (a, Ts) =
+      quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT)));
+
+    fun unif (T1, T2) (env as (tye, _)) =
+      (case pairself (`is_paramT o deref tye) (T1, T2) of
+        ((true, TVar (xi, S)), (_, T)) => assign xi T S env
+      | ((_, T), (true, TVar (xi, S))) => assign xi T S env
+      | ((_, Type (a, Ts)), (_, Type (b, Us))) =>
           if a <> b then
-            raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b, tye)
-          else fold unif (Ts ~~ Us) tye_idx
-      | (T, U) => if T = U then tye_idx else raise NO_UNIFIER ("", tye));
+            raise NO_UNIFIER
+              ("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye)
+          else fold unif (Ts ~~ Us) env
+      | ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye));
 
   in unif end;
 
 
 
-(** type inference **)
-
-(* appl_error *)
-
-fun appl_error pp why t T u U =
- ["Type error in application: " ^ why,
-  "",
-  Pretty.string_of (Pretty.block
-    [Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t,
-      Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]),
-  Pretty.string_of (Pretty.block
-    [Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u,
-      Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]),
-  ""];
-
+(** simple type inference **)
 
 (* infer *)
 
-fun infer pp tsig =
+fun infer ctxt =
   let
+    val pp = Syntax.pp ctxt;
+
+
     (* errors *)
 
-    fun unif_failed msg =
-      "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n";
-
     fun prep_output tye bs ts Ts =
       let
-        val (Ts_bTs', ts') = typs_terms_of tye Name.context ~1 (Ts @ map snd bs, ts);
+        val (Ts_bTs', ts') = finish ctxt tye (Ts @ map snd bs, ts);
         val (Ts', Ts'') = chop (length Ts) Ts_bTs';
         fun prep t =
           let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
           in Term.subst_bounds (map Syntax.mark_boundT xs, t) end;
       in (map prep ts', Ts') end;
 
-    fun err_loose i =
-      raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []);
+    fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
+
+    fun unif_failed msg =
+      "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
 
     fun err_appl msg tye bs t T u U =
-      let
-        val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U];
-        val why =
-          (case T' of
-            Type ("fun", _) => "Incompatible operand type"
-          | _ => "Operator not of function type");
-        val text = unif_failed msg ^ cat_lines (appl_error pp why t' T' u' U');
-      in raise TYPE (text, [T', U'], [t', u']) end;
-
-    fun err_constraint msg tye bs t T U =
-      let
-        val ([t'], [T', U']) = prep_output tye bs [t] [T, U];
-        val text = cat_lines
-         [unif_failed msg,
-          "Cannot meet type constraint:", "",
-          Pretty.string_of (Pretty.block
-           [Pretty.str "Term:", Pretty.brk 2, Pretty.term pp t',
-            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T']),
-          Pretty.string_of (Pretty.block
-           [Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp U']), ""];
-      in raise TYPE (text, [T', U'], [t']) end;
+      let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
+      in error (unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n") end;
 
 
     (* main *)
 
-    val unif = unify pp tsig;
-
-    fun inf _ (PConst (_, T)) tye_idx = (T, tye_idx)
-      | inf _ (PFree (_, T)) tye_idx = (T, tye_idx)
-      | inf _ (PVar (_, T)) tye_idx = (T, tye_idx)
-      | inf bs (PBound i) tye_idx =
+    fun inf _ (Const (_, T)) tye_idx = (T, tye_idx)
+      | inf _ (Free (_, T)) tye_idx = (T, tye_idx)
+      | inf _ (Var (_, T)) tye_idx = (T, tye_idx)
+      | inf bs (Bound i) tye_idx =
           (snd (nth bs i handle Subscript => err_loose i), tye_idx)
-      | inf bs (PAbs (x, T, t)) tye_idx =
+      | inf bs (Abs (x, T, t)) tye_idx =
           let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx
-          in (PType ("fun", [T, U]), tye_idx') end
-      | inf bs (PAppl (t, u)) tye_idx =
+          in (T --> U, tye_idx') end
+      | inf bs (t $ u) tye_idx =
           let
             val (T, tye_idx') = inf bs t tye_idx;
             val (U, (tye, idx)) = inf bs u tye_idx';
-            val V = Param (idx, []);
-            val U_to_V = PType ("fun", [U, V]);
-            val tye_idx'' = unif (U_to_V, T) (tye, idx + 1)
+            val V = mk_param idx [];
+            val tye_idx'' = unify ctxt pp (U --> V, T) (tye, idx + 1)
               handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
-          in (V, tye_idx'') end
-      | inf bs (Constraint (t, U)) tye_idx =
-          let val (T, tye_idx') = inf bs t tye_idx in
-            (T,
-             unif (T, U) tye_idx'
-               handle NO_UNIFIER (msg, tye) => err_constraint msg tye bs t T U)
-          end;
+          in (V, tye_idx'') end;
 
   in inf [] end;
 
 
-(* infer_types *)
+(* main interfaces *)
 
-fun infer_types pp tsig check_typs const_type var_type used maxidx raw_ts =
+fun prepare ctxt const_type var_type raw_ts =
   let
-    (*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*)
-    val ts = burrow_types check_typs raw_ts;
+    val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
     val (ts', (_, _, idx)) =
-      fold_map (preterm_of const_type is_param o constrain_vars) ts
+      fold_map (prepare_term const_type o constrain_vars) ts
       (Vartab.empty, Vartab.empty, 0);
+  in (idx, ts') end;
 
-    (*do type inference*)
-    val (tye, _) = fold (snd oo infer pp tsig) ts' (Inttab.empty, idx);
-  in #2 (typs_terms_of tye used maxidx ([], ts')) end;
+fun infer_types ctxt const_type var_type raw_ts =
+  let
+    val (idx, ts) = prepare ctxt const_type var_type raw_ts;
+    val (tye, _) = fold (snd oo infer ctxt) ts (Vartab.empty, idx);
+    val (_, ts') = finish ctxt tye ([], ts);
+  in ts' end;
 
 end;
diff -r f9371c0751f5 -r 2f38fa28e124 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Pure/variable.ML	Mon Sep 13 13:33:44 2010 +0200
@@ -168,7 +168,7 @@
     (case Vartab.lookup types xi of
       NONE =>
         if pattern then NONE
-        else Vartab.lookup binds xi |> Option.map (Type_Infer.polymorphicT o #1)
+        else Vartab.lookup binds xi |> Option.map (Type.mark_polymorphic o #1)
     | some => some)
   end;
 
diff -r f9371c0751f5 -r 2f38fa28e124 src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Tools/misc_legacy.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/Tools/nbe.ML	Mon Sep 13 13:33:44 2010 +0200
@@ -547,13 +547,13 @@
 
 fun normalize thy program ((vs0, (vs, ty)), t) deps =
   let
+    val ctxt = Syntax.init_pretty_global thy;
     val ty' = typ_of_itype program vs0 ty;
     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);
-    val string_of_term =
-      Syntax.string_of_term (Config.put show_types true (Syntax.init_pretty_global thy));
+      singleton
+        (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE))
+        (Type.constraint ty' t);
+    val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
     fun check_tvars t =
       if null (Term.add_tvars t []) then t
       else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
diff -r f9371c0751f5 -r 2f38fa28e124 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Mon Sep 13 13:33:44 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 f9371c0751f5 -r 2f38fa28e124 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Mon Sep 13 11:13:25 2010 +0200
+++ b/src/ZF/ind_syntax.ML	Mon Sep 13 13:33:44 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