| changeset 63616 | ff66974e31be |
| parent 62922 | 96691631c1eb |
| child 64556 | 851ae0e7b09c |
--- 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)) =