# HG changeset patch
# User wenzelm
# Date 1365771254 -7200
# Node ID c8f2bad67dbbe5e0887fea050ca6090d7b825376
# Parent  0539e75b41704dd8be4ead2bd83e96a99eba7829
tuned signature;
tuned comments;

diff -r 0539e75b4170 -r c8f2bad67dbb src/Pure/envir.ML
--- a/src/Pure/envir.ML	Fri Apr 12 12:20:51 2013 +0200
+++ b/src/Pure/envir.ML	Fri Apr 12 14:54:14 2013 +0200
@@ -19,11 +19,11 @@
   val insert_sorts: env -> sort list -> sort list
   val genvars: string -> env * typ list -> env * term list
   val genvar: string -> env * typ -> env * term
-  val lookup: env * (indexname * typ) -> term option
-  val lookup': tenv * (indexname * typ) -> term option
-  val update: ((indexname * typ) * term) * env -> env
+  val lookup1: tenv -> indexname * typ -> term option
+  val lookup: env -> indexname * typ -> term option
+  val update: (indexname * typ) * term -> env -> env
   val above: env -> int -> bool
-  val vupdate: ((indexname * typ) * term) * env -> env
+  val vupdate: (indexname * typ) * term -> env -> env
   val norm_type_same: Type.tyenv -> typ Same.operation
   val norm_types_same: Type.tyenv -> typ list Same.operation
   val norm_type: Type.tyenv -> typ -> typ
@@ -114,19 +114,17 @@
     NONE => NONE
   | SOME (U, t) => if check (T, U) then SOME t else var_clash xi T U);
 
-(* When dealing with environments produced by matching instead *)
-(* of unification, there is no need to chase assigned TVars.   *)
-(* In this case, we can simply ignore the type substitution    *)
-(* and use = instead of eq_type.                               *)
-
-fun lookup' (tenv, p) = lookup_check (op =) tenv p;
+(*When dealing with environments produced by matching instead
+  of unification, there is no need to chase assigned TVars.
+  In this case, we can simply ignore the type substitution
+  and use = instead of eq_type.*)
+val lookup1 = lookup_check (op =);
 
-fun lookup2 (tyenv, tenv) =
-  lookup_check (Type.eq_type tyenv) tenv;
+fun lookup2 (tyenv, tenv) = lookup_check (Type.eq_type tyenv) tenv;
 
-fun lookup (Envir {tenv, tyenv, ...}, p) = lookup2 (tyenv, tenv) p;
+fun lookup (Envir {tenv, tyenv, ...}) = lookup2 (tyenv, tenv);
 
-fun update (((xi, T), t), Envir {maxidx, tenv, tyenv}) =
+fun update ((xi, T), t) (Envir {maxidx, tenv, tyenv}) =
   Envir {maxidx = maxidx, tenv = Vartab.update_new (xi, (T, t)) tenv, tyenv = tyenv};
 
 (*Determine if the least index updated exceeds lim*)
@@ -135,16 +133,16 @@
   (case Vartab.min_key tyenv of SOME (_, i) => i > lim | NONE => true);
 
 (*Update, checking Var-Var assignments: try to suppress higher indexes*)
-fun vupdate ((aU as (a, U), t), env as Envir {tyenv, ...}) =
+fun vupdate (aU as (a, U), t) (env as Envir {tyenv, ...}) =
   (case t of
     Var (nT as (name', T)) =>
       if a = name' then env     (*cycle!*)
       else if Term_Ord.indexname_ord (a, name') = LESS then
-        (case lookup (env, nT) of  (*if already assigned, chase*)
-          NONE => update ((nT, Var (a, T)), env)
-        | SOME u => vupdate ((aU, u), env))
-      else update ((aU, t), env)
-  | _ => update ((aU, t), env));
+        (case lookup env nT of  (*if already assigned, chase*)
+          NONE => update (nT, Var (a, T)) env
+        | SOME u => vupdate (aU, u) env)
+      else update (aU, t) env
+  | _ => update (aU, t) env);
 
 
 
@@ -168,7 +166,7 @@
 fun norm_term1 tenv : term Same.operation =
   let
     fun norm (Var v) =
-          (case lookup' (tenv, v) of
+          (case lookup1 tenv v of
             SOME u => Same.commit norm u
           | NONE => raise Same.SAME)
       | norm (Abs (a, T, body)) = Abs (a, T, norm body)
@@ -229,7 +227,7 @@
 fun head_norm env =
   let
     fun norm (Var v) =
-        (case lookup (env, v) of
+        (case lookup env v of
           SOME u => head_norm env u
         | NONE => raise Same.SAME)
       | norm (Abs (a, T, body)) = Abs (a, T, norm body)
@@ -309,7 +307,7 @@
 
 fun subst_term1 tenv = Term_Subst.map_aterms_same
   (fn Var v =>
-        (case lookup' (tenv, v) of
+        (case lookup1 tenv v of
           SOME u => u
         | NONE => raise Same.SAME)
     | _ => raise Same.SAME);
@@ -320,7 +318,7 @@
     fun subst (Const (a, T)) = Const (a, substT T)
       | subst (Free (a, T)) = Free (a, substT T)
       | subst (Var (xi, T)) =
-          (case lookup' (tenv, (xi, T)) of
+          (case lookup1 tenv (xi, T) of
             SOME u => u
           | NONE => Var (xi, substT T))
       | subst (Bound _) = raise Same.SAME
diff -r 0539e75b4170 -r c8f2bad67dbb src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri Apr 12 12:20:51 2013 +0200
+++ b/src/Pure/pattern.ML	Fri Apr 12 14:54:14 2013 +0200
@@ -93,7 +93,7 @@
   else ()
 
 fun occurs(F,t,env) =
-    let fun occ(Var (G, T))   = (case Envir.lookup (env, (G, T)) of
+    let fun occ(Var (G, T))   = (case Envir.lookup env (G, T) of
                                  SOME(t) => occ t
                                | NONE    => F=G)
           | occ(t1$t2)      = occ t1 orelse occ t2
@@ -152,7 +152,7 @@
 
 fun mknewhnf(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), mkhnf (binders, is, G, js)) env' end;
 
 
 (*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
@@ -189,7 +189,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), mkhnf (binders, js, H, ks)) env'
                       in (app(H,ls),env'') end
                  | _  => raise Pattern))
         and prs(s::ss,env,d,binders) =
@@ -219,12 +219,12 @@
   let fun ff(F,Fty,is,G as (a,_),Gty,js) =
             if subset (op =) (js, is)
             then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
-                 in Envir.update (((F, Fty), t), env) end
+                 in Envir.update ((F, Fty), t) env end
             else let val ks = inter (op =) js is
                      val Hty = type_of_G env (Fty,length is,map (idx is) ks)
                      val (env',H) = Envir.genvar a (env,Hty)
                      fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
-                 in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
+                 in Envir.update ((G, Gty), lam js) (Envir.update ((F, Fty), lam is) env')
                  end;
   in if Term_Ord.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
 
@@ -273,7 +273,7 @@
 and flexrigid thy (params as (env,binders,F,Fty,is,t)) =
       if occurs(F,t,env) then (ocheck_fail thy (F,t,binders,env); raise Unif)
       else (let val (u,env') = proj(t,env,binders,is)
-            in Envir.update (((F, Fty), mkabs (binders, is, u)), env') end
+            in Envir.update ((F, Fty), mkabs (binders, is, u)) env' end
             handle Unif => (proj_fail thy params; raise Unif));
 
 fun unify thy = unif thy [];
@@ -319,7 +319,7 @@
     fun mtch k (instsp as (tyinsts,insts)) = fn
         (Var(ixn,T), t)  =>
           if k > 0 andalso Term.is_open t then raise MATCH
-          else (case Envir.lookup' (insts, (ixn, T)) of
+          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)
@@ -374,7 +374,7 @@
     in case ph of
          Var(ixn,T) =>
            let val is = ints_of pargs
-           in case Envir.lookup' (itms, (ixn, T)) of
+           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
                           else raise MATCH
diff -r 0539e75b4170 -r c8f2bad67dbb src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Apr 12 12:20:51 2013 +0200
+++ b/src/Pure/proofterm.ML	Fri Apr 12 14:54:14 2013 +0200
@@ -468,7 +468,7 @@
      (Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
         SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvars t []),
    map_filter (fn (ixnT as (_, T)) =>
-     (Envir.lookup (env, ixnT); NONE) handle TYPE _ =>
+     (Envir.lookup env ixnT; NONE) handle TYPE _ =>
         SOME (ixnT, Free ("dummy", T))) (Term.add_vars t [])) t;
 
 fun norm_proof env =
diff -r 0539e75b4170 -r c8f2bad67dbb src/Pure/unify.ML
--- a/src/Pure/unify.ML	Fri Apr 12 12:20:51 2013 +0200
+++ b/src/Pure/unify.ML	Fri Apr 12 14:54:14 2013 +0200
@@ -120,7 +120,7 @@
             (*no need to lookup: v has no assignment*)
           else
             (seen := w :: !seen;
-             case Envir.lookup (env, (w, T)) of
+             case Envir.lookup env (w, T) of
                NONE => false
              | SOME t => occur t)
       | occur (Abs (_, _, body)) = occur body
@@ -133,7 +133,7 @@
   (case t of
     f $ _ => head_of_in (env, f)
   | Var vT =>
-      (case Envir.lookup (env, vT) of
+      (case Envir.lookup env vT of
         SOME u => head_of_in (env, u)
       | NONE => t)
   | _ => t);
@@ -187,7 +187,7 @@
           else if Term.eq_ix (v, w) then Rigid
           else
             (seen := w :: !seen;
-             case Envir.lookup (env, (w, T)) of
+             case Envir.lookup env (w, T) of
                NONE => NoOcc
              | SOME t => occur t)
       | occur (Abs (_, _, body)) = occur body
@@ -239,7 +239,7 @@
     (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)
-        in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end
+        in Envir.update (vT, Logic.rlist_abs (rbinder, u)) env end
     | Nonrigid => raise ASSIGN
     | Rigid => raise CANTUNIFY)
   end;
@@ -310,7 +310,7 @@
 
 (* 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 (env, Var v) = (case Envir.lookup env v of NONE => false | _ => true)
   | changed _ = false;
 
 
@@ -429,8 +429,8 @@
     val Ts = binder_types env T;
     fun new_dset (u', (env', dpairs')) =
       (*if v was updated to s, must unify s with u' *)
-      (case Envir.lookup (env', vT) of
-        NONE => (Envir.update ((vT, types_abs (Ts, u')), env'), dpairs')
+      (case Envir.lookup env' vT of
+        NONE => (Envir.update (vT, types_abs (Ts, u')) env', dpairs')
       | SOME s => (env', ([], s, types_abs (Ts, u')) :: dpairs'));
   in
     Seq.map new_dset (matchcopy thy (#1 v) (rbinder, targs, u, (env, dpairs)))
@@ -447,7 +447,7 @@
     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)
-      in Envir.vupdate ((vT, Logic.rlist_abs (rbinder, u)), env) end
+      in Envir.vupdate (vT, Logic.rlist_abs (rbinder, u)) env end
   end;
 
 
@@ -536,7 +536,7 @@
       let
         val (env', v') = Envir.genvar (#1 v) (env, map #T args ---> U);
         val body = list_comb (v', map (Bound o #j) args);
-        val env2 = Envir.vupdate ((((v, T), types_abs (Ts, body)), env'));
+        val env2 = Envir.vupdate ((v, T), types_abs (Ts, body)) env';
         (*the vupdate affects ts' if they contain v*)
       in (env2, Envir.norm_term env2 (list_comb (v', ts'))) end
   end;
@@ -669,10 +669,10 @@
     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'' = Envir.vupdate ((wU, type_abs (env', U, var)), env');
+    val env'' = Envir.vupdate (wU, type_abs (env', U, var)) env';
   in
     if vT = wU then env''  (*the other update would be identical*)
-    else Envir.vupdate ((vT, type_abs (env', T, var)), env'')
+    else Envir.vupdate (vT, type_abs (env', T, var)) env''
   end;