tuned -- maxidx unused;

--- a/src/Pure/Proof/reconstruct.ML	Fri Aug 05 20:26:13 2016 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Fri Aug 05 20:45:58 2016 +0200
@@ -307,7 +307,7 @@
   (map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts)
   (forall_intr_vfs prop);
 
-val head_norm = Envir.head_norm (Envir.empty 0);
+val head_norm = Envir.head_norm Envir.init;
 
 fun prop_of0 Hs (PBound i) = nth Hs i
   | prop_of0 Hs (Abst (s, SOME T, prf)) =

--- a/src/Pure/envir.ML	Fri Aug 05 20:26:13 2016 +0200
+++ b/src/Pure/envir.ML	Fri Aug 05 20:45:58 2016 +0200
@@ -221,7 +221,7 @@
   else norm_term2 envir;
 
 fun norm_term envir t = norm_term_same envir t handle Same.SAME => t;
-fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t;
+fun beta_norm t = if Term.has_abs t then norm_term init t else t;
 
 end;