# HG changeset patch
# User wenzelm
# Date 1470422758 -7200
# Node ID ff66974e31be82a7c3f8df0ea60b6fada1d20642
# Parent  d786d54efc70feb22ac12821b9af79f67a33d59f
tuned -- maxidx unused;

diff -r d786d54efc70 -r ff66974e31be src/Pure/Proof/reconstruct.ML
--- 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)) =
diff -r d786d54efc70 -r ff66974e31be src/Pure/envir.ML
--- 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;