# HG changeset patch
# User wenzelm
# Date 1369426021 -7200
# Node ID 31224df6e52f749f1623d765913edd481f081046
# Parent  ac7830871177aa1e76a7c833f4a9999e7e56db6d# Parent  f8cd460772241b4f595e85b1cfbbf2e3d3d7852a
merged

diff -r ac7830871177 -r 31224df6e52f src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Fri May 24 22:07:01 2013 +0200
@@ -3411,7 +3411,7 @@
         (term_of_float_float_option_list o float_float_option_list_of_term) t
     | _ => bad t;
 
-  val normalize = eval o Envir.beta_norm o Pattern.eta_long [];
+  val normalize = eval o Envir.beta_norm o Envir.eta_long [];
 
 in Thm.cterm_of thy (Logic.mk_equals (t, normalize t)) end
 *}
diff -r ac7830871177 -r 31224df6e52f src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri May 24 22:07:01 2013 +0200
@@ -110,7 +110,7 @@
     (* The result of the quantifier elimination *)
     val (th, tac) = case (prop_of pre_thm) of
         Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
-    let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
+    let val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
     in
           ((pth RS iffD2) RS pre_thm,
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
diff -r ac7830871177 -r 31224df6e52f src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Fri May 24 22:07:01 2013 +0200
@@ -85,7 +85,7 @@
     (* The result of the quantifier elimination *)
     val (th, tac) = case prop_of pre_thm of
         Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
-    let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1)
+    let val pth = linr_oracle (ctxt, Envir.eta_long [] t1)
     in 
           (trace_msg ("calling procedure with term:\n" ^
              Syntax.string_of_term ctxt t1);
diff -r ac7830871177 -r 31224df6e52f src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri May 24 22:07:01 2013 +0200
@@ -133,8 +133,8 @@
     let val pth =
           (* If quick_and_dirty then run without proof generation as oracle*)
              if Config.get ctxt quick_and_dirty
-             then mirfr_oracle (false, cterm_of thy (Pattern.eta_long [] t1))
-             else mirfr_oracle (true, cterm_of thy (Pattern.eta_long [] t1))
+             then mirfr_oracle (false, cterm_of thy (Envir.eta_long [] t1))
+             else mirfr_oracle (true, cterm_of thy (Envir.eta_long [] t1))
     in 
           (trace_msg ("calling procedure with term:\n" ^
              Syntax.string_of_term ctxt t1);
diff -r ac7830871177 -r 31224df6e52f src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/List.thy	Fri May 24 22:07:01 2013 +0200
@@ -641,7 +641,7 @@
       (case dest_case t of
         SOME (x, T, i, cont) =>
           let
-            val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
+            val (vs, body) = strip_abs (Envir.eta_long (map snd bound_vs) cont)
             val x' = incr_boundvars (length vs) x
             val eqs' = map (incr_boundvars (length vs)) eqs
             val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
diff -r ac7830871177 -r 31224df6e52f src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri May 24 22:07:01 2013 +0200
@@ -196,7 +196,7 @@
       | NONE =>
           let
             val (f, args) = strip_comb t
-            val args = map (Pattern.eta_long []) args
+            val args = map (Envir.eta_long []) args
             val _ = @{assert} (fastype_of t = body_type (fastype_of t))
             val f' = lookup_pred f
             val Ts = case f' of
@@ -232,7 +232,7 @@
                   in (resvar, (resname :: names', prem :: prems')) end))
           end
   in
-    map (apfst Envir.eta_contract) (flatten' (Pattern.eta_long [] t) (names, prems))
+    map (apfst Envir.eta_contract) (flatten' (Envir.eta_long [] t) (names, prems))
   end;
 
 (* FIXME: create new predicate name -- does not avoid nameclashing *)
diff -r ac7830871177 -r 31224df6e52f src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri May 24 22:07:01 2013 +0200
@@ -76,7 +76,7 @@
 fun flatten constname atom (defs, thy) =
   if is_compound atom then
     let
-      val atom = Envir.beta_norm (Pattern.eta_long [] atom)
+      val atom = Envir.beta_norm (Envir.eta_long [] atom)
       val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
         ((Long_Name.base_name constname) ^ "_aux")
       val full_constname = Sign.full_bname thy constname
diff -r ac7830871177 -r 31224df6e52f src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri May 24 22:07:01 2013 +0200
@@ -851,7 +851,7 @@
    let
     val cpth = 
        if Config.get ctxt quick_and_dirty
-       then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
+       then oracle (ctxt, Envir.beta_norm (Envir.eta_long [] (term_of (Thm.dest_arg p))))
        else Conv.arg_conv (conv ctxt) p
     val p' = Thm.rhs_of cpth
     val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
diff -r ac7830871177 -r 31224df6e52f src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Fri May 24 22:07:01 2013 +0200
@@ -125,9 +125,9 @@
 
 fun add_atom (t : term) (m : Rat.rat) (p : (term * Rat.rat) list, i : Rat.rat) :
              (term * Rat.rat) list * Rat.rat =
-  case AList.lookup Pattern.aeconv p t of
+  case AList.lookup Envir.aeconv p t of
       NONE   => ((t, m) :: p, i)
-    | SOME n => (AList.update Pattern.aeconv (t, Rat.add n m) p, i);
+    | SOME n => (AList.update Envir.aeconv (t, Rat.add n m) p, i);
 
 (* decompose nested multiplications, bracketing them to the right and combining
    all their coefficients
@@ -320,7 +320,7 @@
 
 fun subst_term ([] : (term * term) list) (t : term) = t
   | subst_term pairs                     t          =
-      (case AList.lookup Pattern.aeconv pairs t of
+      (case AList.lookup Envir.aeconv pairs t of
         SOME new =>
           new
       | NONE     =>
@@ -672,7 +672,7 @@
 fun negated_term_occurs_positively (terms : term list) : bool =
   List.exists
     (fn (Trueprop $ (Const (@{const_name Not}, _) $ t)) =>
-      member Pattern.aeconv terms (Trueprop $ t)
+      member Envir.aeconv terms (Trueprop $ t)
       | _ => false)
     terms;
 
diff -r ac7830871177 -r 31224df6e52f src/HOL/ex/SVC_Oracle.thy
--- a/src/HOL/ex/SVC_Oracle.thy	Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy	Fri May 24 22:07:01 2013 +0200
@@ -57,7 +57,7 @@
         case t of
             Free _  => t  (*but not existing Vars, lest the names clash*)
           | Bound _ => t
-          | _ => (case AList.lookup Pattern.aeconv (!pairs) t of
+          | _ => (case AList.lookup Envir.aeconv (!pairs) t of
                       SOME v => v
                     | NONE   => insert t)
     (*abstraction of a numeric literal*)
diff -r ac7830871177 -r 31224df6e52f src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Fri May 24 22:07:01 2013 +0200
@@ -458,8 +458,8 @@
 fun trace_msg ctxt msg =
   if Config.get ctxt LA_Data.trace then tracing msg else ();
 
-val union_term = union Pattern.aeconv;
-val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'));
+val union_term = union Envir.aeconv;
+val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Envir.aeconv (t, t'));
 
 fun add_atoms (lhs, _, _, rhs, _, _) =
   union_term (map fst lhs) o union_term (map fst rhs);
@@ -572,7 +572,7 @@
 end;
 
 fun coeff poly atom =
-  AList.lookup Pattern.aeconv poly atom |> the_default 0;
+  AList.lookup Envir.aeconv poly atom |> the_default 0;
 
 fun integ(rlhs,r,rel,rrhs,s,d) =
 let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
diff -r ac7830871177 -r 31224df6e52f src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/Provers/hypsubst.ML	Fri May 24 22:07:01 2013 +0200
@@ -224,7 +224,7 @@
               |> Logic.strip_assums_concl
               |> Data.dest_Trueprop |> Data.dest_imp;
             val (r', tac) =
-              if Pattern.aeconv (hyp, hyp')
+              if Envir.aeconv (hyp, hyp')
               then (r, imp_intr_tac i THEN rotate_tac ~1 i)
               else (*leave affected hyps at end*) (r + 1, imp_intr_tac i);
           in
diff -r ac7830871177 -r 31224df6e52f src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/Provers/splitter.ML	Fri May 24 22:07:01 2013 +0200
@@ -139,7 +139,7 @@
 
 fun mk_cntxt_splitthm t tt T =
   let fun repl lev t =
-    if Pattern.aeconv(incr_boundvars lev tt, t) then Bound lev
+    if Envir.aeconv(incr_boundvars lev tt, t) then Bound lev
     else case t of
         (Abs (v, T2, t)) => Abs (v, T2, repl (lev+1) t)
       | (Bound i) => Bound (if i>=lev then i+1 else i)
diff -r ac7830871177 -r 31224df6e52f src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/Pure/drule.ML	Fri May 24 22:07:01 2013 +0200
@@ -470,7 +470,7 @@
 fun eta_long_conversion ct =
   Thm.transitive
     (beta_eta_conversion ct)
-    (Thm.symmetric (beta_eta_conversion (cterm_fun (Pattern.eta_long []) ct)));
+    (Thm.symmetric (beta_eta_conversion (cterm_fun (Envir.eta_long []) ct)));
 
 (*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*)
 fun eta_contraction_rule th =
diff -r ac7830871177 -r 31224df6e52f src/Pure/envir.ML
--- a/src/Pure/envir.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/Pure/envir.ML	Fri May 24 22:07:01 2013 +0200
@@ -31,8 +31,13 @@
   val norm_term: env -> term -> term
   val beta_norm: term -> term
   val head_norm: env -> term -> term
+  val eta_long: typ list -> term -> term
   val eta_contract: term -> term
   val beta_eta_contract: term -> term
+  val aeconv: term * term -> bool
+  val body_type: env -> int -> typ -> typ
+  val binder_types: env -> int -> typ -> typ list
+  val strip_type: env -> int -> typ -> typ list * typ
   val fastype: env -> typ list -> term -> typ
   val subst_type_same: Type.tyenv -> typ Same.operation
   val subst_term_types_same: Type.tyenv -> term Same.operation
@@ -221,7 +226,7 @@
 end;
 
 
-(*Put a term into head normal form for unification.*)
+(* head normal form for unification *)
 
 fun head_norm env =
   let
@@ -239,7 +244,25 @@
   in Same.commit norm end;
 
 
-(*Eta-contract a term (fully)*)
+(* eta-long beta-normal form *)
+
+fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
+  | eta_long Ts t =
+      (case strip_comb t of
+        (Abs _, _) => eta_long Ts (beta_norm t)
+      | (u, ts) =>
+          let
+            val Us = binder_types (fastype_of1 (Ts, t));
+            val i = length Us;
+            val long = eta_long (rev Us @ Ts);
+          in
+            fold_rev (Term.abs o pair "x") Us
+              (list_comb (incr_boundvars i u,
+                map (long o incr_boundvars i) ts @ map (long o Bound) (i - 1 downto 0)))
+          end);
+
+
+(* full eta contraction *)
 
 local
 
@@ -268,10 +291,30 @@
 fun eta_contract t =
   if Term.has_abs t then Same.commit eta t else t;
 
+end;
+
 val beta_eta_contract = eta_contract o beta_norm;
 
-end;
+fun aeconv (t, u) = t aconv u orelse eta_contract t aconv eta_contract u;
+
 
+fun body_type _ 0 T = T
+  | body_type env n (Type ("fun", [_, T])) = body_type env (n - 1) T
+  | body_type env n (T as TVar v) =
+      (case Type.lookup (type_env env) v of
+        NONE => T
+      | SOME T' => body_type env n T')
+  | body_type _ _ T = T;
+
+fun binder_types _ 0 _ = []
+  | binder_types env n (Type ("fun", [T, U])) = T :: binder_types env (n - 1) U
+  | binder_types env n (TVar v) =
+      (case Type.lookup (type_env env) v of
+        NONE => []
+      | SOME T' => binder_types env n T')
+  | binder_types _ _ _ = [];
+
+fun strip_type n env T = (binder_types n env T, body_type n env T);
 
 (*finds type of term without checking that combinations are consistent
   Ts holds types of bound variables*)
@@ -292,7 +335,6 @@
   in fast end;
 
 
-
 (** plain substitution -- without variable chasing **)
 
 local
diff -r ac7830871177 -r 31224df6e52f src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/Pure/pattern.ML	Fri May 24 22:07:01 2013 +0200
@@ -10,13 +10,9 @@
 TODO: optimize red by special-casing it
 *)
 
-infix aeconv;
-
 signature PATTERN =
 sig
   val trace_unify_fail: bool Unsynchronized.ref
-  val aeconv: term * term -> bool
-  val eta_long: typ list -> term -> term
   val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   val first_order_match: theory -> term * term
     -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
@@ -24,6 +20,7 @@
   val matchess: theory -> term list * term list -> bool
   val equiv: theory -> term * term -> bool
   val matches_subterm: theory -> term * term -> bool
+  val unify_types: theory -> typ * typ -> Envir.env -> Envir.env
   val unify: theory -> term * term -> Envir.env -> Envir.env
   val first_order: term -> bool
   val pattern: term -> bool
@@ -140,7 +137,7 @@
 (* split_type ([T1,....,Tn]---> T,n,[]) = ([Tn,...,T1],T) *)
 fun split_type (T,0,Ts)                    = (Ts,T)
   | split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts)
-  | split_type _                           = error("split_type");
+  | split_type _                           = raise Fail "split_type";
 
 fun type_of_G env (T, n, is) =
   let
@@ -148,11 +145,11 @@
     val (Ts, U) = split_type (Envir.norm_type tyenv T, n, []);
   in map (nth Ts) is ---> U end;
 
-fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js));
+fun mk_hnf (binders,is,G,js) = mkabs (binders, is, app(G,js));
 
-fun mknewhnf(env,binders,is,F as (a,_),T,js) =
+fun mk_new_hnf(env,binders,is,F as (a,_),T,js) =
   let val (env',G) = Envir.genvar a (env,type_of_G env (T,length is,js))
-  in Envir.update ((F, T), mkhnf (binders, is, G, js)) env' end;
+  in Envir.update ((F, T), mk_hnf (binders, is, G, js)) env' end;
 
 
 (*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
@@ -189,7 +186,7 @@
                           val Hty = type_of_G env (Fty,length js,ks)
                           val (env',H) = Envir.genvar a (env,Hty)
                           val env'' =
-                            Envir.update ((F, Fty), mkhnf (binders, js, H, ks)) env'
+                            Envir.update ((F, Fty), mk_hnf (binders, js, H, ks)) env'
                       in (app(H,ls),env'') end
                  | _  => raise Pattern))
         and prs(s::ss,env,d,binders) =
@@ -207,13 +204,13 @@
     let fun mk([],[],_)        = []
           | mk(i::is,j::js, k) = if (i:int) = j then k :: mk(is,js,k-1)
                                         else mk(is,js,k-1)
-          | mk _               = error"mk_ff_list"
+          | mk _               = raise Fail "mk_ff_list"
     in mk(is,js,length is-1) end;
 
 fun flexflex1(env,binders,F,Fty,is,js) =
   if is=js then env
   else let val ks = mk_ff_list(is,js)
-       in mknewhnf(env,binders,is,F,Fty,ks) end;
+       in mk_new_hnf(env,binders,is,F,Fty,ks) end;
 
 fun flexflex2(env,binders,F,Fty,is,G,Gty,js) =
   let fun ff(F,Fty,is,G as (a,_),Gty,js) =
@@ -238,7 +235,7 @@
 fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of
       (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
          let val name = if ns = "" then nt else ns
-         in unif thy ((name,Ts)::binders) (ts,tt) env end
+         in unif thy ((name,Ts)::binders) (ts,tt) (unify_types thy (Ts, Tt) env) end
     | (Abs(ns,Ts,ts),t) => unif thy ((ns,Ts)::binders) (ts,(incr t)$Bound(0)) env
     | (t,Abs(nt,Tt,tt)) => unif thy ((nt,Tt)::binders) ((incr t)$Bound(0),tt) env
     | p => cases thy (binders,env,p)
@@ -279,27 +276,6 @@
 fun unify thy = unif thy [];
 
 
-(* put a term into eta long beta normal form *)
-fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
-  | eta_long Ts t =
-      (case strip_comb t of
-        (Abs _, _) => eta_long Ts (Envir.beta_norm t)
-      | (u, ts) =>
-          let
-            val Us = binder_types (fastype_of1 (Ts, t));
-            val i = length Us;
-          in
-            fold_rev (Term.abs o pair "x") Us
-              (list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
-                (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
-          end);
-
-
-(*Tests whether 2 terms are alpha/eta-convertible and have same type.
-  Note that Consts and Vars may have more than one type.*)
-fun t aeconv u = t aconv u orelse
-  Envir.eta_contract t aconv Envir.eta_contract u;
-
 
 (*** Matching ***)
 
@@ -322,7 +298,7 @@
           else (case Envir.lookup1 insts (ixn, T) of
                   NONE => (typ_match thy (T, fastype_of t) tyinsts,
                            Vartab.update_new (ixn, (T, t)) insts)
-                | SOME u => if t aeconv u then instsp else raise MATCH)
+                | SOME u => if Envir.aeconv (t, u) then instsp else raise MATCH)
       | (Free (a,T), Free (b,U)) =>
           if a=b then (typ_match thy (T,U) tyinsts, insts) else raise MATCH
       | (Const (a,T), Const (b,U))  =>
@@ -376,7 +352,7 @@
            let val is = ints_of pargs
            in case Envir.lookup1 itms (ixn, T) of
                 NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj))
-              | SOME u => if obj aeconv (red u is []) then env
+              | SOME u => if Envir.aeconv (obj, red u is []) then env
                           else raise MATCH
            end
        | _ =>
diff -r ac7830871177 -r 31224df6e52f src/Pure/tactical.ML
--- a/src/Pure/tactical.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/Pure/tactical.ML	Fri May 24 22:07:01 2013 +0200
@@ -340,7 +340,7 @@
         fun diff st' =
             Thm.nprems_of st' - d <= 0   (*the subgoal no longer exists*)
             orelse
-             not (Pattern.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
+             not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
     in  Seq.filter diff (tac i st)  end
     handle General.Subscript => Seq.empty  (*no subgoal i*);
 
diff -r ac7830871177 -r 31224df6e52f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/Pure/thm.ML	Fri May 24 22:07:01 2013 +0200
@@ -888,7 +888,7 @@
     shyps = sorts,
     hyps = [],
     tpairs = [],
-    prop = Logic.mk_equals (t, Pattern.eta_long [] t)});
+    prop = Logic.mk_equals (t, Envir.eta_long [] t)});
 
 (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   The bound variable will be named "a" (since x will be something like x320)
@@ -1384,7 +1384,7 @@
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
     val (_, asms, concl) = Logic.assum_problems (~1, Bi);
   in
-    (case find_index (fn asm => Pattern.aeconv (asm, concl)) asms of
+    (case find_index (fn asm => Envir.aeconv (asm, concl)) asms of
       ~1 => raise THM ("eq_assumption", 0, [state])
     | n =>
         Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der,
diff -r ac7830871177 -r 31224df6e52f src/Pure/unify.ML
--- a/src/Pure/unify.ML	Fri May 24 16:43:37 2013 +0200
+++ b/src/Pure/unify.ML	Fri May 24 22:07:01 2013 +0200
@@ -19,6 +19,8 @@
   val trace_simp: bool Config.T
   val trace_types_raw: Config.raw
   val trace_types: bool Config.T
+  val hounifiers: theory * Envir.env * ((term * term) list) ->
+    (Envir.env * (term * term) list) Seq.seq
   val unifiers: theory * Envir.env * ((term * term) list) ->
     (Envir.env * (term * term) list) Seq.seq
   val smash_unifiers: theory -> (term * term) list -> Envir.env -> Envir.env Seq.seq
@@ -48,34 +50,10 @@
 val trace_types = Config.bool trace_types_raw;
 
 
-type binderlist = (string*typ) list;
+type binderlist = (string * typ) list;
 
 type dpair = binderlist * term * term;
 
-fun body_type env =
-  let
-    val tyenv = Envir.type_env env;
-    fun bT (Type ("fun", [_, T])) = bT T
-      | bT (T as TVar v) =
-          (case Type.lookup tyenv v of
-            NONE => T
-          | SOME T' => bT T')
-      | bT T = T;
-  in bT end;
-
-fun binder_types env =
-  let
-    val tyenv = Envir.type_env env;
-    fun bTs (Type ("fun", [T, U])) = T :: bTs U
-      | bTs (TVar v) =
-          (case Type.lookup tyenv v of
-            NONE => []
-          | SOME T' => bTs T')
-      | bTs _ = [];
-  in bTs end;
-
-fun strip_type env T = (binder_types env T, body_type env T);
-
 fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t;
 
 
@@ -128,13 +106,13 @@
   in occurs ts end;
 
 
-(* f(a1,...,an)  ---->   (f,  [a1,...,an])  using the assignments*)
-fun head_of_in (env, t) : term =
+(* f a1 ... an  ---->  f  using the assignments*)
+fun head_of_in env t =
   (case t of
-    f $ _ => head_of_in (env, f)
+    f $ _ => head_of_in env f
   | Var vT =>
       (case Envir.lookup env vT of
-        SOME u => head_of_in (env, u)
+        SOME u => head_of_in env u
       | NONE => t)
   | _ => t);
 
@@ -192,7 +170,7 @@
              | SOME t => occur t)
       | occur (Abs (_, _, body)) = occur body
       | occur (t as f $ _) =  (*switch to nonrigid search?*)
-          (case head_of_in (env, f) of
+          (case head_of_in env f of
             Var (w,_) => (*w is not assigned*)
               if Term.eq_ix (v, w) then Rigid
               else nonrigid t
@@ -205,20 +183,14 @@
 exception ASSIGN;  (*Raised if not an assignment*)
 
 
-fun unify_types thy (T, U, env) =
-  if T = U then env
-  else
-    let
-      val Envir.Envir {maxidx, tenv, tyenv} = env;
-      val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx);
-    in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
-    handle Type.TUNIFY => raise CANTUNIFY;
+fun unify_types thy TU env =
+  Pattern.unify_types thy TU env handle Pattern.Unif => raise CANTUNIFY;
 
-fun test_unify_types thy (args as (T, U, _)) =
+fun test_unify_types thy (T, U) env =
   let
     val str_of = Syntax.string_of_typ_global thy;
     fun warn () = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);
-    val env' = unify_types thy args;
+    val env' = unify_types thy (T, U) env;
   in if is_TVar T orelse is_TVar U then warn () else (); env' end;
 
 (*Is the term eta-convertible to a single variable with the given rbinder?
@@ -234,11 +206,11 @@
 (*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
   If v occurs rigidly then nonunifiable.
   If v occurs nonrigidly then must use full algorithm. *)
-fun assignment thy (env, rbinder, t, u) =
+fun assignment thy (rbinder, t, u) env =
   let val vT as (v,T) = get_eta_var (rbinder, 0, t) in
     (case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
       NoOcc =>
-        let val env = unify_types thy (body_type env T, fastype env (rbinder, u), env)
+        let val env = unify_types thy (Envir.body_type env ~1 T, fastype env (rbinder, u)) env
         in Envir.update (vT, Logic.rlist_abs (rbinder, u)) env end
     | Nonrigid => raise ASSIGN
     | Rigid => raise CANTUNIFY)
@@ -250,20 +222,20 @@
   Checks that binders have same length, since terms should be eta-normal;
     if not, raises TERM, probably indicating type mismatch.
   Uses variable a (unless the null string) to preserve user's naming.*)
-fun new_dpair thy (rbinder, Abs (a, T, body1), Abs (b, U, body2), env) =
+fun new_dpair thy (rbinder, Abs (a, T, body1), Abs (b, U, body2)) env =
       let
-        val env' = unify_types thy (T, U, env);
+        val env' = unify_types thy (T, U) env;
         val c = if a = "" then b else a;
-      in new_dpair thy ((c,T) :: rbinder, body1, body2, env') end
-  | new_dpair _ (_, Abs _, _, _) = raise TERM ("new_dpair", [])
-  | new_dpair _ (_, _, Abs _, _) = raise TERM ("new_dpair", [])
-  | new_dpair _ (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
+      in new_dpair thy ((c,T) :: rbinder, body1, body2) env' end
+  | new_dpair _ (_, Abs _, _) _ = raise TERM ("new_dpair", [])
+  | new_dpair _ (_, _, Abs _) _ = raise TERM ("new_dpair", [])
+  | new_dpair _ (rbinder, t1, t2) env = ((rbinder, t1, t2), env);
 
 
 fun head_norm_dpair thy (env, (rbinder, t, u)) : dpair * Envir.env =
   new_dpair thy (rbinder,
     eta_norm env (rbinder, Envir.head_norm env t),
-    eta_norm env (rbinder, Envir.head_norm env u), env);
+    eta_norm env (rbinder, Envir.head_norm env u)) env;
 
 
 
@@ -287,31 +259,31 @@
     (case (head_of t, head_of u) of
       (Var (_, T), Var (_, U)) =>
         let
-          val T' = body_type env T and U' = body_type env U;
-          val env = unify_types thy (T', U', env);
+          val T' = Envir.body_type env ~1 T and U' = Envir.body_type env ~1 U;
+          val env = unify_types thy (T', U') env;
         in (env, dp :: flexflex, flexrigid) end
     | (Var _, _) =>
-        ((assignment thy (env, rbinder,t,u), flexflex, flexrigid)
+        ((assignment thy (rbinder,t,u) env, flexflex, flexrigid)
           handle ASSIGN => (env, flexflex, dp :: flexrigid))
     | (_, Var _) =>
-        ((assignment thy (env, rbinder, u, t), flexflex, flexrigid)
+        ((assignment thy (rbinder, u, t) env, flexflex, flexrigid)
           handle ASSIGN => (env, flexflex, (rbinder, u, t) :: flexrigid))
     | (Const (a, T), Const (b, U)) =>
-        if a = b then SIMRANDS (t, u, unify_types thy (T, U, env))
+        if a = b then SIMRANDS (t, u, unify_types thy (T, U) env)
         else raise CANTUNIFY
     | (Bound i, Bound j) =>
         if i = j then SIMRANDS (t, u, env) else raise CANTUNIFY
     | (Free (a, T), Free (b, U)) =>
-        if a = b then SIMRANDS (t, u, unify_types thy (T, U, env))
+        if a = b then SIMRANDS (t, u, unify_types thy (T, U) env)
         else raise CANTUNIFY
     | _ => raise CANTUNIFY)
   end;
 
 
 (* changed(env,t) checks whether the head of t is a variable assigned in env*)
-fun changed (env, f $ _) = changed (env, f)
-  | changed (env, Var v) = (case Envir.lookup env v of NONE => false | _ => true)
-  | changed _ = false;
+fun changed env (f $ _) = changed env f
+  | changed env (Var v) = (case Envir.lookup env v of NONE => false | _ => true)
+  | changed _ _ = false;
 
 
 (*Recursion needed if any of the 'head variables' have been updated
@@ -321,7 +293,7 @@
     val all as (env', flexflex, flexrigid) = fold_rev (SIMPL0 thy) dpairs (env, [], []);
     val dps = flexrigid @ flexflex;
   in
-    if exists (fn (_, t, u) => changed (env', t) orelse changed (env', u)) dps
+    if exists (fn (_, t, u) => changed env' t orelse changed env' u) dps
     then SIMPL thy (env', dps) else all
   end;
 
@@ -344,7 +316,7 @@
   | types_abs (T :: Ts, u) = Abs ("", T, types_abs (Ts, u));
 
 (*Abstraction over the binder of a type*)
-fun type_abs (env, T, t) = types_abs (binder_types env T, t);
+fun type_abs (env, T, t) = types_abs (Envir.binder_types env ~1 T, t);
 
 
 (*MATCH taking "big steps".
@@ -370,15 +342,15 @@
         fun copyargs [] = Seq.cons ([], ed) Seq.empty
           | copyargs (uarg :: uargs) = Seq.maps (copycons uarg) (copyargs uargs);
         val (uhead, uargs) = strip_comb u;
-        val base = body_type env (fastype env (rbinder, uhead));
+        val base = Envir.body_type env ~1 (fastype env (rbinder, uhead));
         fun joinargs (uargs', ed') = (list_comb (uhead, uargs'), ed');
         (*attempt projection on argument with given typ*)
         val Ts = map (curry (fastype env) rbinder) targs;
         fun projenv (head, (Us, bary), targ, tail) =
           let
             val env =
-              if trace_tps then test_unify_types thy (base, bary, env)
-              else unify_types thy (base, bary, env)
+              if trace_tps then test_unify_types thy (base, bary) env
+              else unify_types thy (base, bary) env
           in
             Seq.make (fn () =>
               let
@@ -399,7 +371,7 @@
           | make_projs _ = raise TERM ("make_projs", u::targs);
         (*try projections and imitation*)
         fun matchfun ((bvar,T,targ)::projs) =
-             (projenv(bvar, strip_type env T, targ, matchfun projs))
+             (projenv(bvar, Envir.strip_type env ~1 T, targ, matchfun projs))
           | matchfun [] = (*imitation last of all*)
             (case uhead of
          Const _ => Seq.map joinargs (copyargs uargs)
@@ -426,7 +398,7 @@
 fun MATCH thy (env, (rbinder, t, u), dpairs) : (Envir.env * dpair list) Seq.seq =
   let
     val (Var (vT as (v, T)), targs) = strip_comb t;
-    val Ts = binder_types env T;
+    val Ts = Envir.binder_types env ~1 T;
     fun new_dset (u', (env', dpairs')) =
       (*if v was updated to s, must unify s with u' *)
       (case Envir.lookup env' vT of
@@ -446,7 +418,7 @@
   let val vT as (v, T) = get_eta_var (rbinder, 0, t) in
     if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
     else
-      let val env = unify_types thy (body_type env T, fastype env (rbinder, u), env)
+      let val env = unify_types thy (Envir.body_type env ~1 T, fastype env (rbinder, u)) env
       in Envir.vupdate (vT, Logic.rlist_abs (rbinder, u)) env end
   end;
 
@@ -526,7 +498,7 @@
 fun clean_term banned (env,t) =
   let
     val (Var (v, T), ts) = strip_comb t;
-    val (Ts, U) = strip_type env T
+    val (Ts, U) = Envir.strip_type env ~1 T
     and js = length ts - 1  downto 0;
     val args = sort_args (fold_rev (change_arg banned) (flexargs (js, ts, Ts)) [])
     val ts' = map #t args;
@@ -668,7 +640,7 @@
   let
     val vT as (v, T) = var_head_of (env, t)
     and wU as (w, U) = var_head_of (env, u);
-    val (env', var) = Envir.genvar (#1 v) (env, body_type env T);
+    val (env', var) = Envir.genvar (#1 v) (env, Envir.body_type env ~1 T);
     val env'' = Envir.vupdate (wU, type_abs (env', U, var)) env';
   in
     if vT = wU then env''  (*the other update would be identical*)