# HG changeset patch
# User huffman
# Date 1291215054 28800
# Node ID f2c9ebbe04aaeb514348bab1fb50654f6b0beb94
# Parent  225698654b2aafd39e2a3f747d1cd736c3b53c41# Parent  df8c7dc30214daded172e409934a8e89b0639bd5
merged

diff -r 225698654b2a -r f2c9ebbe04aa src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/CCL/CCL.thy	Wed Dec 01 06:50:54 2010 -0800
@@ -233,7 +233,7 @@
          | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
          | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s)
            val T = Sign.the_const_type thy (Sign.intern_const thy sy);
-           val arity = length (fst (strip_type T))
+           val arity = length (binder_types T)
        in sy ^ (arg_str arity name "") end
 
   fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b")
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Complex_Main.thy
--- a/src/HOL/Complex_Main.thy	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Complex_Main.thy	Wed Dec 01 06:50:54 2010 -0800
@@ -10,6 +10,9 @@
   Ln
   Taylor
   Deriv
+uses "~~/src/Tools/subtyping.ML"
 begin
 
+setup Subtyping.setup
+
 end
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/HOL.thy	Wed Dec 01 06:50:54 2010 -0800
@@ -1796,9 +1796,8 @@
 setup {*
   Code_Preproc.map_pre (fn simpset =>
     simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
-      (fn thy => fn _ => fn Const (_, T) => case strip_type T
-        of (Type _ :: _, _) => SOME @{thm eq_equal}
-         | _ => NONE)])
+      (fn thy => fn _ =>
+        fn Const (_, Type ("fun", [Type _, _])) => SOME @{thm eq_equal} | _ => NONE)])
 *}
 
 
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/HOLCF/Tools/holcf_library.ML
--- a/src/HOL/HOLCF/Tools/holcf_library.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/HOLCF/Tools/holcf_library.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -83,7 +83,7 @@
 
 fun mk_cabs t =
   let val T = fastype_of t
-  in cabs_const (Term.domain_type T, Term.range_type T) $ t end
+  in cabs_const (Term.dest_funT T) $ t end
 
 (* builds the expression (% v1 v2 .. vn. rhs) *)
 fun lambdas [] rhs = rhs
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Import/proof_kernel.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -415,9 +415,6 @@
 
 val mk_var = Free
 
-fun dom_rng (Type("fun",[dom,rng])) = (dom,rng)
-  | dom_rng _ = raise ERR "dom_rng" "Not a functional type"
-
 fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty)
 
 local
@@ -1481,7 +1478,7 @@
                         _ $ (Const(@{const_name HOL.eq},_) $ x $ y) => (x,y)
                       | _ => raise ERR "mk_COMB" "Second theorem not an equality"
         val fty = type_of f
-        val (fd,fr) = dom_rng fty
+        val (fd,fr) = Term.dest_funT fty
         val comb_thm' = Drule.instantiate'
                             [SOME (ctyp_of thy fd),SOME (ctyp_of thy fr)]
                             [SOME (cterm_of thy f),SOME (cterm_of thy g),
@@ -1789,7 +1786,7 @@
         val (f,g) = case concl_of th1 of
                         _ $ (Const(@{const_name HOL.eq},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
                       | _ => raise ERR "mk_ABS" "Bad conclusion"
-        val (fd,fr) = dom_rng (type_of f)
+        val (fd,fr) = Term.dest_funT (type_of f)
         val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm
         val th2 = Thm.forall_intr cv th1
         val th3 = th2 COMP abs_thm'
@@ -1835,7 +1832,7 @@
                 in
                     fold_rev (fn v => fn th =>
                               let
-                                  val cdom = fst (dom_rng (fst (dom_rng cty)))
+                                  val cdom = fst (Term.dest_funT (fst (Term.dest_funT cty)))
                                   val vty  = type_of v
                                   val newcty = inst_type cdom vty cty
                                   val cc = cterm_of thy (Const(cname,newcty))
@@ -1991,7 +1988,7 @@
                                fun dest_eta_abs (Abs(x,xT,body)) = (x,xT,body)
                                  | dest_eta_abs body =
                                    let
-                                       val (dT,rT) = dom_rng (type_of body)
+                                       val (dT,rT) = Term.dest_funT (type_of body)
                                    in
                                        ("x",dT,body $ Bound 0)
                                    end
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/IsaMakefile	Wed Dec 01 06:50:54 2010 -0800
@@ -385,6 +385,7 @@
 	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
 
 HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
+  $(SRC)/Tools/subtyping.ML \
   Archimedean_Field.thy \
   Complex.thy \
   Complex_Main.thy \
@@ -408,9 +409,9 @@
   Series.thy \
   SupInf.thy \
   Taylor.thy \
-  Transcendental.thy \
+  Tools/SMT/smt_real.ML \
   Tools/float_syntax.ML \
-  Tools/SMT/smt_real.ML
+  Transcendental.thy
 
 $(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES)
 	@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL
@@ -1030,25 +1031,24 @@
 $(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy	\
   Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy		\
   ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy	\
-  ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradoxon.thy ex/CTL.thy   \
-  ex/Chinese.thy \
-  ex/Classical.thy ex/CodegenSML_Test.thy ex/Coercion_Examples.thy	\
-  ex/Coherent.thy ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy	\
-  ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy		\
-  ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
-  ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\
-  ex/Iff_Oracle.thy ex/Induction_Schema.thy ex/InductiveInvariant.thy	\
-  ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy		\
-  ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy		\
-  ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy	\
-  ex/Normalization_by_Evaluation.thy ex/Numeral.thy ex/PER.thy		\
-  ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy		\
-  ex/Quickcheck_Lattice_Examples.thy ex/Quicksort.thy ex/ROOT.ML	\
-  ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy			\
-  ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
-  ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy		\
-  ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy	\
-  ex/Unification.thy ex/While_Combinator_Example.thy			\
+  ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradoxon.thy ex/CTL.thy	\
+  ex/Chinese.thy ex/Classical.thy ex/CodegenSML_Test.thy		\
+  ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy		\
+  ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy	\
+  ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy	\
+  ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy		\
+  ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy	\
+  ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy		\
+  ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy	\
+  ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
+  ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy	\
+  ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
+  ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy		\
+  ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy		\
+  ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy	\
+  ex/SVC_Oracle.thy ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy	\
+  ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy	\
+  ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy	\
   ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML	\
   ex/svc_test.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -274,7 +274,7 @@
           fun perm_arg (dt, x) =
             let val T = type_of x
             in if is_rec_type dt then
-                let val (Us, _) = strip_type T
+                let val Us = binder_types T
                 in list_abs (map (pair "x") Us,
                   Free (nth perm_names_types' (body_index dt)) $ pi $
                     list_comb (x, map (fn (i, U) =>
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -334,14 +334,14 @@
         val t :: ts2 = drop i ts;
         val names = List.foldr OldTerm.add_term_names
           (map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1;
-        val (Ts, dT) = split_last (take (i+1) (fst (strip_type T)));
+        val (Ts, dT) = split_last (take (i+1) (binder_types T));
 
         fun pcase [] [] [] gr = ([], gr)
           | pcase ((cname, cargs)::cs) (t::ts) (U::Us) gr =
               let
                 val j = length cargs;
                 val xs = Name.variant_list names (replicate j "x");
-                val Us' = take j (fst (strip_type U));
+                val Us' = take j (binder_types U);
                 val frees = map2 (curry Free) xs Us';
                 val (cp, gr0) = invoke_codegen thy defs dep module false
                   (list_comb (Const (cname, Us' ---> dT), frees)) gr;
@@ -385,26 +385,33 @@
 
 (* code generators for terms and types *)
 
-fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of
-   (c as Const (s, T), ts) =>
-     (case Datatype_Data.info_of_case thy s of
+fun datatype_codegen thy defs dep module brack t gr =
+  (case strip_comb t of
+    (c as Const (s, T), ts) =>
+      (case Datatype_Data.info_of_case thy s of
         SOME {index, descr, ...} =>
-          if is_some (get_assoc_code thy (s, T)) then NONE else
-          SOME (pretty_case thy defs dep module brack
-            (#3 (the (AList.lookup op = descr index))) c ts gr )
-      | NONE => case (Datatype_Data.info_of_constr thy (s, T), strip_type T) of
-        (SOME {index, descr, ...}, (_, U as Type (tyname, _))) =>
-          if is_some (get_assoc_code thy (s, T)) then NONE else
-          let
-            val SOME (tyname', _, constrs) = AList.lookup op = descr index;
-            val SOME args = AList.lookup op = constrs s
-          in
-            if tyname <> tyname' then NONE
-            else SOME (pretty_constr thy defs
-              dep module brack args c ts (snd (invoke_tycodegen thy defs dep module false U gr)))
-          end
-      | _ => NONE)
- | _ => NONE);
+          if is_some (get_assoc_code thy (s, T)) then NONE
+          else
+            SOME (pretty_case thy defs dep module brack
+              (#3 (the (AList.lookup op = descr index))) c ts gr)
+      | NONE =>
+          (case (Datatype_Data.info_of_constr thy (s, T), body_type T) of
+            (SOME {index, descr, ...}, U as Type (tyname, _)) =>
+              if is_some (get_assoc_code thy (s, T)) then NONE
+              else
+                let
+                  val SOME (tyname', _, constrs) = AList.lookup op = descr index;
+                  val SOME args = AList.lookup op = constrs s;
+                in
+                  if tyname <> tyname' then NONE
+                  else
+                    SOME
+                      (pretty_constr thy defs
+                        dep module brack args c ts
+                        (snd (invoke_tycodegen thy defs dep module false U gr)))
+                end
+          | _ => NONE))
+  | _ => NONE);
 
 fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
       (case Datatype_Data.get_info thy s of
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -72,7 +72,7 @@
 fun info_of_constr thy (c, T) =
   let
     val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
-    val hint = case strip_type T of (_, Type (tyco, _)) => SOME tyco | _ => NONE;
+    val hint = case body_type T of Type (tyco, _) => SOME tyco | _ => NONE;
     val default = if null tab then NONE
       else SOME (snd (Library.last_elem tab))
         (*conservative wrt. overloaded constructors*);
@@ -387,7 +387,7 @@
     fun type_of_constr (cT as (_, T)) =
       let
         val frees = OldTerm.typ_tfrees T;
-        val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T
+        val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type T))
           handle TYPE _ => no_constr cT
         val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
         val _ = if length frees <> length vs then no_constr cT else ();
@@ -412,8 +412,8 @@
       (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
 
     val cs = map (apsnd (map norm_constr)) raw_cs;
-    val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
-      o fst o strip_type;
+    val dtyps_of_typ =
+      map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) o binder_types;
     val dt_names = map fst cs;
 
     fun mk_spec (i, (tyco, constr)) = (i, (tyco,
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Tools/Datatype/datatype_prop.ML
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -385,7 +385,7 @@
 
         fun mk_clause ((f, g), (cname, _)) =
           let
-            val (Ts, _) = strip_type (fastype_of f);
+            val Ts = binder_types (fastype_of f);
             val tnames = Name.variant_list used (make_tnames Ts);
             val frees = map Free (tnames ~~ Ts)
           in
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -25,7 +25,7 @@
 fun prf_of thm =
   Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
 
-fun is_unit t = snd (strip_type (fastype_of t)) = HOLogic.unitT;
+fun is_unit t = body_type (fastype_of t) = HOLogic.unitT;
 
 fun tname_of (Type (s, _)) = s
   | tname_of _ = "";
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -485,7 +485,7 @@
 
 fun is_pred thy constname = (body_type (Sign.the_const_type thy constname) = HOLogic.boolT);
 
-fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = @{typ bool})
+fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool})
   | is_predT _ = false
 
 (*** check if a term contains only constructor functions ***)
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -87,17 +87,6 @@
     Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u
   end;
 
-fun dest_funT (Type ("fun",[S, T])) = (S, T)
-  | dest_funT T = raise TYPE ("dest_funT", [T], [])
- 
-fun mk_fun_comp (t, u) =
-  let
-    val (_, B) = dest_funT (fastype_of t)
-    val (C, A) = dest_funT (fastype_of u)
-  in
-    Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
-  end;
-
 fun dest_randomT (Type ("fun", [@{typ Random.seed},
   Type (@{type_name Product_Type.prod}, [Type (@{type_name Product_Type.prod}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
   | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -81,7 +81,7 @@
 (* TODO: does not work with higher order functions yet *)
 fun mk_rewr_eq (func, pred) =
   let
-    val (argTs, resT) = (strip_type (fastype_of func))
+    val (argTs, resT) = strip_type (fastype_of func)
     val nctxt =
       Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
     val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -234,9 +234,6 @@
     (Abs a) => snd (Term.dest_abs a)
   | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
 
-fun dest_fun_type (Type("fun", [T, S])) = (T, S)
-  | dest_fun_type _ = error "dest_fun_type"
-
 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
 
 (* We apply apply_rsp only in case if the type needs lifting.
@@ -296,7 +293,7 @@
     | SOME (rel $ _ $ (rep $ (abs $ _))) =>
         let
           val thy = ProofContext.theory_of ctxt;
-          val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
+          val (ty_a, ty_b) = dest_funT (fastype_of abs);
           val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
         in
           case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of
@@ -483,8 +480,8 @@
     (Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
       let
         val thy = ProofContext.theory_of ctxt
-        val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
-        val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
+        val (ty_b, ty_a) = dest_funT (fastype_of r1)
+        val (ty_c, ty_d) = dest_funT (fastype_of a2)
         val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
         val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
         val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Tools/SMT/smt_utils.ML
--- a/src/HOL/Tools/SMT/smt_utils.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_utils.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -10,7 +10,6 @@
   val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
 
   (* types *)
-  val split_type: typ -> typ * typ
   val dest_funT: int -> typ -> typ list * typ
 
   (* terms *)
@@ -57,8 +56,6 @@
 
 (* types *)
 
-fun split_type T = (Term.domain_type T, Term.range_type T)
-
 val dest_funT =
   let
     fun dest Ts 0 T = (rev Ts, T)
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Tools/SMT/z3_model.ML
--- a/src/HOL/Tools/SMT/z3_model.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_model.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -131,7 +131,7 @@
       end)
 
 and trans_array T a =
-  let val (dT, rT) = U.split_type T
+  let val (dT, rT) = Term.dest_funT T
   in
     (case a of
       Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t))
@@ -151,11 +151,11 @@
 
 fun mk_update ([], u) _ = u
   | mk_update ([t], u) f =
-      uncurry mk_fun_upd (U.split_type (Term.fastype_of f)) $ f $ t $ u
+      uncurry mk_fun_upd (Term.dest_funT (Term.fastype_of f)) $ f $ t $ u
   | mk_update (t :: ts, u) f =
       let
-        val (dT, rT) = U.split_type (Term.fastype_of f)
-        val (dT', rT') = U.split_type rT
+        val (dT, rT) = Term.dest_funT (Term.fastype_of f)
+        val (dT', rT') = Term.dest_funT rT
       in
         mk_fun_upd dT rT $ f $ t $
           mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT')))
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Tools/SMT/z3_proof_methods.ML
--- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -36,14 +36,14 @@
 
 fun mk_inv_of ctxt ct =
   let
-    val (dT, rT) = U.split_type (U.typ_of ct)
+    val (dT, rT) = Term.dest_funT (U.typ_of ct)
     val inv = U.certify ctxt (mk_inv_into dT rT)
     val univ = U.certify ctxt (mk_univ dT)
   in Thm.mk_binop inv univ ct end
 
 fun mk_inj_prop ctxt ct =
   let
-    val (dT, rT) = U.split_type (U.typ_of ct)
+    val (dT, rT) = Term.dest_funT (U.typ_of ct)
     val inj = U.certify ctxt (mk_inj_on dT rT)
     val univ = U.certify ctxt (mk_univ dT)
   in U.mk_cprop (Thm.mk_binop inj ct univ) end
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/hologic.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -8,6 +8,7 @@
 sig
   val typeS: sort
   val typeT: typ
+  val mk_comp: term * term -> term
   val boolN: string
   val boolT: typ
   val Trueprop: term
@@ -142,6 +143,16 @@
 val typeT = Type_Infer.anyT typeS;
 
 
+(* functions *)
+
+fun mk_comp (f, g) =
+  let
+    val fT = fastype_of f;
+    val gT = fastype_of g;
+    val compT = fT --> gT --> domain_type gT --> range_type fT;
+  in Const ("Fun.comp", compT) $ f $ g end;
+
+
 (* bool and set *)
 
 val boolN = "HOL.bool";
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/recfun_codegen.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -34,7 +34,8 @@
 
 fun avoid_value thy [thm] =
       let val (_, T) = Code.const_typ_eqn thy thm
-      in if null (Term.add_tvarsT T []) orelse (null o fst o strip_type) T
+      in
+        if null (Term.add_tvarsT T []) orelse null (binder_types T)
         then [thm]
         else [Code.expand_eta thy 1 thm]
       end
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/record.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -1013,18 +1013,9 @@
     SOME u_name => u_name = s
   | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
 
-fun mk_comp f g =
-  let
-    val X = fastype_of g;
-    val A = domain_type X;
-    val B = range_type X;
-    val C = range_type (fastype_of f);
-    val T = (B --> C) --> (A --> B) --> A --> C;
-  in Const (@{const_name Fun.comp}, T) $ f $ g end;
-
 fun mk_comp_id f =
   let val T = range_type (fastype_of f)
-  in mk_comp (Const (@{const_name Fun.id}, T --> T)) f end;
+  in HOLogic.mk_comp (Const (@{const_name Fun.id}, T --> T), f) end;
 
 fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
   | get_upd_funs _ = [];
@@ -1037,10 +1028,10 @@
       let
         (* FIXME fresh "f" (!?) *)
         val T = domain_type (fastype_of upd);
-        val lhs = mk_comp acc (upd $ Free ("f", T));
+        val lhs = HOLogic.mk_comp (acc, upd $ Free ("f", T));
         val rhs =
           if is_sel_upd_pair thy acc upd
-          then mk_comp (Free ("f", T)) acc
+          then HOLogic.mk_comp (Free ("f", T), acc)
           else mk_comp_id acc;
         val prop = lhs === rhs;
         val othm =
@@ -1061,11 +1052,11 @@
     (* FIXME fresh "f" (!?) *)
     val f = Free ("f", domain_type (fastype_of u));
     val f' = Free ("f'", domain_type (fastype_of u'));
-    val lhs = mk_comp (u $ f) (u' $ f');
+    val lhs = HOLogic.mk_comp (u $ f, u' $ f');
     val rhs =
       if comp
-      then u $ mk_comp f f'
-      else mk_comp (u' $ f') (u $ f);
+      then u $ HOLogic.mk_comp (f, f')
+      else HOLogic.mk_comp (u' $ f', u $ f);
     val prop = lhs === rhs;
     val othm =
       Goal.prove (ProofContext.init_global thy) [] [] prop
@@ -1870,7 +1861,7 @@
          (fn _ => fn eq_def => tac eq_def) eq_def)
     |-> (fn eq_def => fn thy => thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
     |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
-    |> ensure_random_record ext_tyco vs (fst ext) ((fst o strip_type o snd) ext)
+    |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
   end;
 
 
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/Tools/smallvalue_generators.ML
--- a/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -18,17 +18,6 @@
 
 (** general term functions **)
 
-fun dest_funT (Type ("fun",[S, T])) = (S, T)
-  | dest_funT T = raise TYPE ("dest_funT", [T], [])
- 
-fun mk_fun_comp (t, u) =
-  let
-    val (_, B) = dest_funT (fastype_of t)
-    val (C, A) = dest_funT (fastype_of u)
-  in
-    Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
-  end;
-
 fun mk_measure f =
   let
     val Type ("fun", [T, @{typ nat}]) = fastype_of f 
@@ -139,7 +128,7 @@
   let
     val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
     val eqs = mk_equations thy descr vs tycos (names, auxnames) (Ts, Us)
-    fun mk_single_measure T = mk_fun_comp (@{term "Code_Numeral.nat_of"},
+    fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
       Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
     fun mk_termination_measure T =
       let
diff -r 225698654b2a -r f2c9ebbe04aa src/HOL/ex/Coercion_Examples.thy
--- a/src/HOL/ex/Coercion_Examples.thy	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/ex/Coercion_Examples.thy	Wed Dec 01 06:50:54 2010 -0800
@@ -5,12 +5,9 @@
 *)
 
 theory Coercion_Examples
-imports Main
-uses "~~/src/Tools/subtyping.ML"
+imports Complex_Main
 begin
 
-setup Subtyping.setup
-
 (* Error messages test *)
 
 consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat"
diff -r 225698654b2a -r f2c9ebbe04aa src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/Pure/Isar/code.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -358,7 +358,7 @@
  of SOME ty => ty
   | NONE => (Type.strip_sorts o Sign.the_const_type thy) c;
 
-fun args_number thy = length o fst o strip_type o const_typ thy;
+fun args_number thy = length o binder_types o const_typ thy;
 
 fun subst_signature thy c ty =
   let
@@ -391,7 +391,7 @@
     fun last_typ c_ty ty =
       let
         val tfrees = Term.add_tfreesT ty [];
-        val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
+        val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type ty))
           handle TYPE _ => no_constr thy "bad type" c_ty
         val _ = if tyco = "fun" then no_constr thy "bad type" c_ty else ();
         val _ = if has_duplicates (eq_fst (op =)) vs
@@ -420,7 +420,7 @@
         val the_v = the o AList.lookup (op =) (vs ~~ vs');
         val ty' = map_type_tfree (fn (v, _) => TFree (the_v v)) ty;
         val (vs'', _) = logical_typscheme thy (c, ty');
-      in (c, (vs'', (fst o strip_type) ty')) end;
+      in (c, (vs'', binder_types ty')) end;
     val c' :: cs' = map (analyze_constructor thy) cs;
     val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
     val vs = Name.names Name.context Name.aT sorts;
@@ -444,7 +444,7 @@
   | _ => error ("Not an abstract type: " ^ tyco);
  
 fun get_type_of_constr_or_abstr thy c =
-  case (snd o strip_type o const_typ thy) c
+  case (body_type o const_typ thy) c
    of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco
         in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
     | _ => NONE;
@@ -517,7 +517,7 @@
       | check n (Const (c_ty as (c, ty))) =
           if allow_pats then let
             val c' = AxClass.unoverload_const thy c_ty
-          in if n = (length o fst o strip_type o subst_signature thy c') ty
+          in if n = (length o binder_types o subst_signature thy c') ty
             then if allow_consts orelse is_constr thy c'
               then ()
               else bad (quote c ^ " is not a constructor, on left hand side of equation")
@@ -1139,7 +1139,7 @@
     val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;
     val (ws, vs) = chop pos zs;
     val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const);
-    val Ts = (fst o strip_type) T;
+    val Ts = binder_types T;
     val T_cong = nth Ts pos;
     fun mk_prem z = Free (z, T_cong);
     fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
diff -r 225698654b2a -r f2c9ebbe04aa src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/Pure/Proof/extraction.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -135,11 +135,13 @@
 
 val prf_subst_TVars = Proofterm.map_proof_types o typ_subst_TVars;
 
-fun relevant_vars types prop = List.foldr (fn
-      (Var ((a, _), T), vs) => (case strip_type T of
-        (_, Type (s, _)) => if member (op =) types s then a :: vs else vs
-      | _ => vs)
-    | (_, vs) => vs) [] (vars_of prop);
+fun relevant_vars types prop =
+  List.foldr
+    (fn (Var ((a, _), T), vs) =>
+        (case body_type T of
+          Type (s, _) => if member (op =) types s then a :: vs else vs
+        | _ => vs)
+      | (_, vs) => vs) [] (vars_of prop);
 
 fun tname_of (Type (s, _)) = s
   | tname_of _ = "";
diff -r 225698654b2a -r f2c9ebbe04aa src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/Pure/codegen.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -664,7 +664,7 @@
                  NONE =>
                    let
                      val _ = message ("expanding definition of " ^ s);
-                     val (Ts, _) = strip_type U;
+                     val Ts = binder_types U;
                      val (args', rhs') =
                        if not (null args) orelse null Ts then (args, rhs) else
                          let val v = Free (new_name rhs "x", hd Ts)
diff -r 225698654b2a -r f2c9ebbe04aa src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/Pure/term.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -48,6 +48,7 @@
   val dest_comb: term -> term * term
   val domain_type: typ -> typ
   val range_type: typ -> typ
+  val dest_funT: typ -> typ * typ
   val binder_types: typ -> typ list
   val body_type: typ -> typ
   val strip_type: typ -> typ list * typ
@@ -283,20 +284,24 @@
   | dest_comb t = raise TERM("dest_comb", [t]);
 
 
-fun domain_type (Type("fun", [T,_])) = T
-and range_type  (Type("fun", [_,T])) = T;
+fun domain_type (Type ("fun", [T, _])) = T;
+
+fun range_type (Type ("fun", [_, U])) = U;
+
+fun dest_funT (Type ("fun", [T, U])) = (T, U)
+  | dest_funT T = raise TYPE ("dest_funT", [T], []);
+
 
 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
-fun binder_types (Type("fun",[S,T])) = S :: binder_types T
-  | binder_types _   =  [];
+fun binder_types (Type ("fun", [T, U])) = T :: binder_types U
+  | binder_types _ = [];
 
 (* maps  [T1,...,Tn]--->T  to T*)
-fun body_type (Type("fun",[S,T])) = body_type T
-  | body_type T   =  T;
+fun body_type (Type ("fun", [_, U])) = body_type U
+  | body_type T = T;
 
 (* maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)  *)
-fun strip_type T : typ list * typ =
-  (binder_types T, body_type T);
+fun strip_type T = (binder_types T, body_type T);
 
 
 (*Compute the type of the term, checking that combinations are well-typed
@@ -707,7 +712,7 @@
             val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
           in ((v, T) :: vs, t') end;
     val ((vs1, t'), (k', used')) = strip_abs t (k, used);
-    val Ts = (fst o chop k' o fst o strip_type o fastype_of) t';
+    val Ts = fst (chop k' (binder_types (fastype_of t')));
     val (vs2, t'') = expand_eta Ts t' used';
   in (vs1 @ vs2, t'') end;
 
@@ -1002,5 +1007,5 @@
 
 end;
 
-structure BasicTerm: BASIC_TERM = Term;
-open BasicTerm;
+structure Basic_Term: BASIC_TERM = Term;
+open Basic_Term;
diff -r 225698654b2a -r f2c9ebbe04aa src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/Tools/Code/code_thingol.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -710,7 +710,7 @@
       else ()
     val arg_typs = Sign.const_typargs thy (c, ty);
     val sorts = Code_Preproc.sortargs eqngr c;
-    val function_typs = (fst o Term.strip_type) ty;
+    val function_typs = Term.binder_types ty;
   in
     ensure_const thy algbr eqngr permissive c
     ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
@@ -724,7 +724,7 @@
   #>> (fn (t, ts) => t `$$ ts)
 and translate_case thy algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
   let
-    fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty;
+    fun arg_types num_args ty = fst (chop num_args (binder_types ty));
     val tys = arg_types num_args (snd c_ty);
     val ty = nth tys t_pos;
     fun mk_constr c t = let val n = Code.args_number thy c
diff -r 225698654b2a -r f2c9ebbe04aa src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Wed Dec 01 06:48:40 2010 -0800
+++ b/src/Tools/subtyping.ML	Wed Dec 01 06:50:54 2010 -0800
@@ -11,6 +11,7 @@
     term list -> term list
   val add_type_map: term -> Context.generic -> Context.generic
   val add_coercion: term -> Context.generic -> Context.generic
+  val gen_coercion: Proof.context -> typ Vartab.table -> (typ * typ) -> term
   val setup: theory -> theory
 end;
 
@@ -86,8 +87,9 @@
 val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi) | _ => false;
 
 
-(* unification *)  (* TODO dup? needed for weak unification *)
+(* unification *)
 
+exception TYPE_INFERENCE_ERROR of unit -> string;
 exception NO_UNIFIER of string * typ Vartab.table;
 
 fun unify weak ctxt =
@@ -185,6 +187,10 @@
 
 (** error messages **)
 
+fun gen_msg err msg = 
+  err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^ 
+  (if msg = "" then "" else ": " ^ msg) ^ "\n";
+
 fun prep_output ctxt tye bs ts Ts =
   let
     val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts);
@@ -195,23 +201,23 @@
   in (map prep ts', Ts') end;
 
 fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
-
-fun inf_failed msg =
-  "Subtype inference failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
+  
+fun unif_failed msg =
+  "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
 
-fun err_appl ctxt msg tye bs t T u U =
+fun subtyping_err_appl_msg ctxt msg tye bs t T u U () =
   let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U]
-  in error (inf_failed msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n") end;
-
-fun err_subtype ctxt msg tye (bs, t $ u, U, V, U') =
-  err_appl ctxt msg tye bs t (U --> V) u U';
+  in msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n" end;
+  
+fun err_appl_msg ctxt msg tye bs t T u U () =
+  let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U]
+  in unif_failed msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n" end;
 
 fun err_list ctxt msg tye Ts =
   let
     val (_, Ts') = prep_output ctxt tye [] [] Ts;
-    val text = cat_lines ([inf_failed msg,
-      "Cannot unify a list of types that should be the same,",
-      "according to suptype dependencies:",
+    val text = cat_lines ([msg,
+      "Cannot unify a list of types that should be the same:",
       (Pretty.string_of (Pretty.list "[" "]" (map (Pretty.typ (Syntax.pp ctxt)) Ts')))]);
   in
     error text
@@ -222,15 +228,15 @@
     val pp = Syntax.pp ctxt;
     val (ts, Ts) = fold
       (fn (bs, t $ u, U, _, U') => fn (ts, Ts) =>
-        let val (t', T') = prep_output ctxt tye bs [t, u] [U, U']
+        let val (t', T') = prep_output ctxt tye bs [t, u] [U', U]
         in (t' :: ts, T' :: Ts) end)
       packs ([], []);
-    val text = cat_lines ([inf_failed msg, "Cannot fullfill subtype constraints:"] @
+    val text = cat_lines ([msg, "Cannot fulfil subtype constraints:"] @
         (map2 (fn [t, u] => fn [T, U] => Pretty.string_of (
           Pretty.block [
             Pretty.typ pp T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2, Pretty.typ pp U,
             Pretty.brk 3, Pretty.str "from function application", Pretty.brk 2,
-            Pretty.block [Pretty.term pp t, Pretty.brk 1, Pretty.term pp u]]))
+            Pretty.block [Pretty.term pp (t $ u)]]))
         ts Ts))
   in
     error text
@@ -240,7 +246,7 @@
 
 (** constraint generation **)
 
-fun generate_constraints ctxt =
+fun generate_constraints ctxt err =
   let
     fun gen cs _ (Const (_, T)) tye_idx = (T, tye_idx, cs)
       | gen cs _ (Free (_, T)) tye_idx = (T, tye_idx, cs)
@@ -257,7 +263,7 @@
             val U = Type_Infer.mk_param idx [];
             val V = Type_Infer.mk_param (idx + 1) [];
             val tye_idx''= strong_unify ctxt (U --> V, T) (tye, idx + 2)
-              handle NO_UNIFIER (msg, tye') => err_appl ctxt msg tye' bs t T u U;
+              handle NO_UNIFIER (msg, tye') => error (gen_msg err msg);
             val error_pack = (bs, t $ u, U, V, U');
           in (V, tye_idx'', ((U', U), error_pack) :: cs'') end;
   in
@@ -270,7 +276,7 @@
 
 exception BOUND_ERROR of string;
 
-fun process_constraints ctxt cs tye_idx =
+fun process_constraints ctxt err cs tye_idx =
   let
     val coes_graph = coes_graph_of ctxt;
     val tmaps = tmaps_of ctxt;
@@ -289,9 +295,8 @@
     (* check whether constraint simplification will terminate using weak unification *)
 
     val _ = fold (fn (TU, error_pack) => fn tye_idx =>
-      (weak_unify ctxt TU tye_idx handle NO_UNIFIER (msg, tye) =>
-        err_subtype ctxt ("Weak unification of subtype constraints fails:\n" ^ msg)
-          tye error_pack)) cs tye_idx;
+      weak_unify ctxt TU tye_idx handle NO_UNIFIER (msg, tye) =>
+        error (gen_msg err ("weak unification of subtype constraints fails\n" ^ msg))) cs tye_idx;
 
 
     (* simplify constraints *)
@@ -310,7 +315,8 @@
                 COVARIANT => (constraint :: cs, tye_idx)
               | CONTRAVARIANT => (swap constraint :: cs, tye_idx)
               | INVARIANT => (cs, strong_unify ctxt constraint tye_idx
-                  handle NO_UNIFIER (msg, tye) => err_subtype ctxt msg tye error_pack));
+                  handle NO_UNIFIER (msg, tye) => 
+                    error (gen_msg err ("failed to unify invariant arguments\n" ^ msg))));
             val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack))
               (fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx)));
             val test_update = is_compT orf is_freeT orf is_fixedvarT;
@@ -348,7 +354,7 @@
           in
             if subsort (S', S) (*TODO check this*)
             then simplify done' todo' (tye', idx)
-            else err_subtype ctxt "Sort mismatch" tye error_pack
+            else error (gen_msg err "sort mismatch")
           end
         and simplify done [] tye_idx = (done, tye_idx)
           | simplify done (((T, U), error_pack) :: todo) (tye_idx as (tye, idx)) =
@@ -356,9 +362,10 @@
                 (Type (a, []), Type (b, [])) =>
                   if a = b then simplify done todo tye_idx
                   else if Graph.is_edge coes_graph (a, b) then simplify done todo tye_idx
-                  else err_subtype ctxt (a ^ " is not a subtype of " ^ b) (fst tye_idx) error_pack
+                  else error (gen_msg err (a ^ " is not a subtype of " ^ b))
               | (Type (a, Ts), Type (b, Us)) =>
-                  if a <> b then err_subtype ctxt "Different constructors" (fst tye_idx) error_pack
+                  if a <> b then error (gen_msg err "different constructors")
+                    (fst tye_idx) error_pack
                   else contract a Ts Us error_pack done todo tye idx
               | (TVar (xi, S), Type (a, Ts as (_ :: _))) =>
                   expand true xi S a Ts error_pack done todo tye idx
@@ -370,8 +377,7 @@
                     exists Type_Infer.is_paramT [T, U]
                   then eliminate [T, U] error_pack done todo tye idx
                   else if exists (is_freeT orf is_fixedvarT) [T, U]
-                  then err_subtype ctxt "Not eliminated free/fixed variables"
-                        (fst tye_idx) error_pack
+                  then error (gen_msg err "not eliminated free/fixed variables")
                   else simplify (((T, U), error_pack) :: done) todo tye_idx);
       in
         simplify [] cs tye_idx
@@ -381,14 +387,22 @@
     (* do simplification *)
 
     val (cs', tye_idx') = simplify_constraints cs tye_idx;
-
-    fun find_error_pack lower T' =
-      map snd (filter (fn ((T, U), _) => if lower then T' = U else T' = T) cs');
+    
+    fun find_error_pack lower T' = map_filter 
+      (fn ((T, U), pack) => if if lower then T' = U else T' = T then SOME pack else NONE) cs';
+      
+    fun find_cycle_packs nodes = 
+      let
+        val (but_last, last) = split_last nodes
+        val pairs = (last, hd nodes) :: (but_last ~~ tl nodes);
+      in
+        map_filter
+          (fn (TU, pack) => if member (op =) pairs TU then SOME pack else NONE)
+          cs'
+      end;
 
     fun unify_list (T :: Ts) tye_idx =
-      fold (fn U => fn tye_idx => strong_unify ctxt (T, U) tye_idx
-        handle NO_UNIFIER (msg, tye) => err_list ctxt msg tye (T :: Ts))
-      Ts tye_idx;
+      fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx;
 
     (*styps stands either for supertypes or for subtypes of a type T
       in terms of the subtype-relation (excluding T itself)*)
@@ -403,7 +417,7 @@
           | extract T (U :: Us) =
               if Graph.is_edge coes_graph (adjust T U) then extract T Us
               else if Graph.is_edge coes_graph (adjust U T) then extract U Us
-              else raise BOUND_ERROR "Uncomparable types in type list";
+              else raise BOUND_ERROR "uncomparable types in type list";
       in
         t_of (extract T Ts)
       end;
@@ -435,7 +449,7 @@
         fun candidates T = inter (op =) (filter restriction (T :: styps sup T));
       in
         (case fold candidates Ts (filter restriction (T :: styps sup T)) of
-          [] => raise BOUND_ERROR ("No " ^ (if sup then "supremum" else "infimum"))
+          [] => raise BOUND_ERROR ("no " ^ (if sup then "supremum" else "infimum"))
         | [T] => t_of T
         | Ts => minmax sup Ts)
       end;
@@ -449,23 +463,45 @@
             val (G'', tye_idx') = (add_edge (T, U) G', tye_idx)
               handle Typ_Graph.CYCLES cycles =>
                 let
-                  val (tye, idx) = fold unify_list cycles tye_idx
+                  val (tye, idx) = 
+                    fold 
+                      (fn cycle => fn tye_idx' => (unify_list cycle tye_idx'
+                        handle NO_UNIFIER (msg, tye) => 
+                          err_bound ctxt 
+                            (gen_msg err ("constraint cycle not unifiable" ^ msg)) (fst tye_idx)
+                            (find_cycle_packs cycle)))
+                      cycles tye_idx
                 in
-                  (*all cycles collapse to one node,
-                    because all of them share at least the nodes x and y*)
-                  collapse (tye, idx) (distinct (op =) (flat cycles)) G
-                end;
+                  collapse (tye, idx) cycles G
+                end
           in
             build_graph G'' cs tye_idx'
           end
-    and collapse (tye, idx) nodes G = (*nodes non-empty list*)
+    and collapse (tye, idx) cycles G = (*nodes non-empty list*)
       let
-        val T = hd nodes;
+        (*all cycles collapse to one node,
+          because all of them share at least the nodes x and y*)
+        val nodes = (distinct (op =) (flat cycles));
+        val T = Type_Infer.deref tye (hd nodes);
         val P = new_imm_preds G nodes;
         val S = new_imm_succs G nodes;
         val G' = Typ_Graph.del_nodes (tl nodes) G;
+        fun check_and_gen super T' =
+          let val U = Type_Infer.deref tye T';
+          in
+            if not (is_typeT T) orelse not (is_typeT U) orelse T = U
+            then if super then (hd nodes, T') else (T', hd nodes)
+            else 
+              if super andalso 
+                Graph.is_edge coes_graph (nameT T, nameT U) then (hd nodes, T')
+              else if not super andalso 
+                Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes)
+              else err_bound ctxt (gen_msg err "cycle elimination produces inconsistent graph")
+                    (fst tye_idx) 
+                    (maps find_cycle_packs cycles @ find_error_pack super T')
+          end;
       in
-        build_graph G' (map (fn x => (x, T)) P @ map (fn x => (T, x)) S) (tye, idx)
+        build_graph G' (map (check_and_gen false) P @ map (check_and_gen true) S) (tye, idx)
       end;
 
     fun assign_bound lower G key (tye_idx as (tye, _)) =
@@ -488,7 +524,8 @@
           val assignment =
             if null bound orelse null not_params then NONE
             else SOME (tightest lower S styps_and_sorts (map nameT not_params)
-                handle BOUND_ERROR msg => err_bound ctxt msg tye (find_error_pack lower key))
+                handle BOUND_ERROR msg => 
+                  err_bound ctxt (gen_msg err msg) tye (find_error_pack lower key))
         in
           (case assignment of
             NONE => tye_idx
@@ -501,9 +538,9 @@
                 in
                   if subset (op = o apfst nameT) (filter is_typeT other_bound, s :: styps true s)
                   then apfst (Vartab.update (xi, T)) tye_idx
-                  else err_bound ctxt ("Assigned simple type " ^ s ^
+                  else err_bound ctxt (gen_msg err ("assigned simple type " ^ s ^
                     " clashes with the upper bound of variable " ^
-                    Syntax.string_of_typ ctxt (TVar(xi, S))) tye (find_error_pack (not lower) key)
+                    Syntax.string_of_typ ctxt (TVar(xi, S)))) tye (find_error_pack (not lower) key)
                 end
               else apfst (Vartab.update (xi, T)) tye_idx)
         end
@@ -519,7 +556,8 @@
           val (tye_idx' as (tye, _)) = fold (assign_lb G) ts tye_idx
             |> fold (assign_ub G) ts;
         in
-          assign_alternating ts (filter (Type_Infer.is_paramT o Type_Infer.deref tye) ts) G tye_idx'
+          assign_alternating ts 
+            (filter (Type_Infer.is_paramT o Type_Infer.deref tye) ts) G tye_idx'
         end;
 
     (*Unify all weakly connected components of the constraint forest,
@@ -531,7 +569,10 @@
           filter (Type_Infer.is_paramT o Type_Infer.deref tye) (Typ_Graph.maximals G);
         val to_unify = map (fn T => T :: get_preds G T) max_params;
       in
-        fold unify_list to_unify tye_idx
+        fold 
+          (fn Ts => fn tye_idx' => unify_list Ts tye_idx'
+            handle NO_UNIFIER (msg, tye) => err_list ctxt (gen_msg err msg) (fst tye_idx) Ts)
+          to_unify tye_idx
       end;
 
     fun solve_constraints G tye_idx = tye_idx
@@ -546,77 +587,73 @@
 
 (** coercion insertion **)
 
+fun gen_coercion ctxt tye (T1, T2) =
+  (case pairself (Type_Infer.deref tye) (T1, T2) of
+    ((Type (a, [])), (Type (b, []))) =>
+        if a = b
+        then Abs (Name.uu, Type (a, []), Bound 0)
+        else
+          (case Symreltab.lookup (coes_of ctxt) (a, b) of
+            NONE => raise Fail (a ^ " is not a subtype of " ^ b)
+          | SOME co => co)
+  | ((Type (a, Ts)), (Type (b, Us))) =>
+        if a <> b
+        then raise Fail ("Different constructors: " ^ a ^ " and " ^ b)
+        else
+          let
+            fun inst t Ts =
+              Term.subst_vars
+                (((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts), []) t;
+            fun sub_co (COVARIANT, TU) = gen_coercion ctxt tye TU
+              | sub_co (CONTRAVARIANT, TU) = gen_coercion ctxt tye (swap TU);
+            fun ts_of [] = []
+              | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
+          in
+            (case Symtab.lookup (tmaps_of ctxt) a of
+              NONE => raise Fail ("No map function for " ^ a ^ " known")
+            | SOME tmap =>
+                let
+                  val used_coes = map sub_co ((snd tmap) ~~ (Ts ~~ Us));
+                in
+                  Term.list_comb
+                    (inst (fst tmap) (ts_of (map fastype_of used_coes)), used_coes)
+                end)
+          end
+  | (T, U) =>
+        if Type.could_unify (T, U)
+        then Abs (Name.uu, T, Bound 0)
+        else raise Fail ("Cannot generate coercion from "
+          ^ Syntax.string_of_typ ctxt T ^ " to " ^ Syntax.string_of_typ ctxt U));
+
 fun insert_coercions ctxt tye ts =
   let
-    fun deep_deref T =
-      (case Type_Infer.deref tye T of
-        Type (a, Ts) => Type (a, map deep_deref Ts)
-      | U => U);
-
-    fun gen_coercion ((Type (a, [])), (Type (b, []))) =
-          if a = b
-          then Abs (Name.uu, Type (a, []), Bound 0)
-          else
-            (case Symreltab.lookup (coes_of ctxt) (a, b) of
-              NONE => raise Fail (a ^ " is not a subtype of " ^ b)
-            | SOME co => co)
-      | gen_coercion ((Type (a, Ts)), (Type (b, Us))) =
-          if a <> b
-          then raise raise Fail ("Different constructors: " ^ a ^ " and " ^ b)
-          else
-            let
-              fun inst t Ts =
-                Term.subst_vars
-                  (((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts), []) t;
-              fun sub_co (COVARIANT, TU) = gen_coercion TU
-                | sub_co (CONTRAVARIANT, TU) = gen_coercion (swap TU);
-              fun ts_of [] = []
-                | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
-            in
-              (case Symtab.lookup (tmaps_of ctxt) a of
-                NONE => raise Fail ("No map function for " ^ a ^ " known")
-              | SOME tmap =>
-                  let
-                    val used_coes = map sub_co ((snd tmap) ~~ (Ts ~~ Us));
-                  in
-                    Term.list_comb
-                      (inst (fst tmap) (ts_of (map fastype_of used_coes)), used_coes)
-                  end)
-            end
-      | gen_coercion (T, U) =
-          if Type.could_unify (T, U)
-          then Abs (Name.uu, T, Bound 0)
-          else raise Fail ("Cannot generate coercion from "
-            ^ Syntax.string_of_typ ctxt T ^ " to " ^ Syntax.string_of_typ ctxt U);
-
     fun insert _ (Const (c, T)) =
-          let val T' = deep_deref T;
+          let val T' = T;
           in (Const (c, T'), T') end
       | insert _ (Free (x, T)) =
-          let val T' = deep_deref T;
+          let val T' = T;
           in (Free (x, T'), T') end
       | insert _ (Var (xi, T)) =
-          let val T' = deep_deref T;
+          let val T' = T;
           in (Var (xi, T'), T') end
       | insert bs (Bound i) =
-          let val T = nth bs i handle Subscript =>
-            raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []);
+          let val T = nth bs i handle Subscript => err_loose i;
           in (Bound i, T) end
       | insert bs (Abs (x, T, t)) =
           let
-            val T' = deep_deref T;
+            val T' = T;
             val (t', T'') = insert (T' :: bs) t;
           in
             (Abs (x, T', t'), T' --> T'')
           end
       | insert bs (t $ u) =
           let
-            val (t', Type ("fun", [U, T])) = insert bs t;
+            val (t', Type ("fun", [U, T])) = apsnd (Type_Infer.deref tye) (insert bs t);
             val (u', U') = insert bs u;
           in
-            if U <> U'
-            then (t' $ (gen_coercion (U', U) $ u'), T)
-            else (t' $ u', T)
+            if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U')
+            then (t' $ u', T)
+            else (t' $ (gen_coercion ctxt tye (U', U) $ u'), T)
           end
   in
     map (fst o insert []) ts
@@ -630,14 +667,40 @@
   let
     val (idx, ts) = Type_Infer.prepare ctxt const_type var_type raw_ts;
 
-    fun gen_all t (tye_idx, constraints) =
-      let
-        val (_, tye_idx', constraints') = generate_constraints ctxt t tye_idx
-      in (tye_idx', constraints' @ constraints) end;
+    fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx)
+      | inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx)
+      | inf _ (t as (Var (_, T))) tye_idx = (t, T, tye_idx)
+      | inf bs (t as (Bound i)) tye_idx =
+          (t, snd (nth bs i handle Subscript => err_loose i), tye_idx)
+      | inf bs (Abs (x, T, t)) tye_idx =
+          let val (t', U, tye_idx') = inf ((x, T) :: bs) t tye_idx
+          in (Abs (x, T, t'), T --> U, tye_idx') end
+      | inf bs (t $ u) tye_idx =
+          let
+            val (t', T, tye_idx') = inf bs t tye_idx;
+            val (u', U, (tye, idx)) = inf bs u tye_idx';
+            val V = Type_Infer.mk_param idx [];
+            val (tu, tye_idx'') = (t' $ u', strong_unify ctxt (U --> V, T) (tye, idx + 1))
+              handle NO_UNIFIER (msg, tye') => 
+                raise TYPE_INFERENCE_ERROR (err_appl_msg ctxt msg tye' bs t T u U);
+          in (tu, V, tye_idx'') end;
 
-    val (tye_idx, constraints) = fold gen_all ts ((Vartab.empty, idx), []);
-    val (tye, _) = process_constraints ctxt constraints tye_idx;
-    val ts' = insert_coercions ctxt tye ts;
+    fun infer_single t (ts, tye_idx) = 
+      let val (t, _, tye_idx') = inf [] t tye_idx;
+      in (ts @ [t], tye_idx') end;
+      
+    val (ts', (tye, _)) = (fold infer_single ts ([], (Vartab.empty, idx))
+      handle TYPE_INFERENCE_ERROR err =>     
+        let
+          fun gen_single t (tye_idx, constraints) =
+            let val (_, tye_idx', constraints') = generate_constraints ctxt err t tye_idx
+            in (tye_idx', constraints' @ constraints) end;
+      
+          val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []);
+          val (tye, idx) = process_constraints ctxt err constraints tye_idx;
+        in 
+          (insert_coercions ctxt tye ts, (tye, idx))
+        end);
 
     val (_, ts'') = Type_Infer.finish ctxt tye ([], ts');
   in ts'' end;
@@ -711,8 +774,8 @@
         Syntax.string_of_term ctxt t ^ ":\n" ^
         Syntax.string_of_typ ctxt (fastype_of t));
 
-    val (Type ("fun", [T1, T2])) = fastype_of t
-      handle Bind => err_coercion ();
+    val (T1, T2) = Term.dest_funT (fastype_of t)
+      handle TYPE _ => err_coercion ();
 
     val a =
       (case T1 of
@@ -738,7 +801,7 @@
         fun complex_coercion tab G (a, b) =
           let
             val path = hd (Graph.irreducible_paths G (a, b))
-            val path' = (fst (split_last path)) ~~ tl path
+            val path' = fst (split_last path) ~~ tl path
           in Abs (Name.uu, Type (a, []),
               fold (fn t => fn u => t $ u) (map (the o Symreltab.lookup tab) path') (Bound 0))
           end;