src/Pure/pattern.ML

   let
     val tyenv = Envir.type_env env;
     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 mknewhnf(env,binders,is,F as (a,_),T,js) =
+fun mk_hnf (binders,is,G,js) = mkabs (binders, is, app(G,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]*)
 fun downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1)
   | downto0 ([], n) = n = ~1;

                           val ks = mk_proj_list js';
                           val ls = map_filter I js'
                           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) =
               let val (s',env1) = pr(s,env,d,binders)
                   val (ss',env2) = prs(ss,env1,d,binders)

     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) =
             if subset (op =) (js, is)
             then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))