--- a/src/Pure/pattern.ML Fri May 24 15:32:02 2013 +0200
+++ b/src/Pure/pattern.ML Fri May 24 16:42:57 2013 +0200
@@ -149,11 +149,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]*)
@@ -190,7 +190,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) =
@@ -214,7 +214,7 @@
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) =