| changeset 18929 | d81435108688 |
| parent 18184 | 43c4589a9a78 |
| child 19305 | 5c16895d548b |
--- a/src/Pure/Proof/reconstruct.ML Mon Feb 06 11:01:28 2006 +0100 +++ b/src/Pure/Proof/reconstruct.ML Mon Feb 06 20:58:54 2006 +0100 @@ -326,7 +326,7 @@ | prop_of0 Hs (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts | prop_of0 _ _ = error "prop_of: partial proof object"; -val prop_of' = Pattern.eta_contract oo (Envir.beta_norm oo prop_of0); +val prop_of' = Envir.beta_eta_contract oo prop_of0; val prop_of = prop_of' [];