# HG changeset patch # User wenzelm # Date 974483452 -3600 # Node ID 97d25c125c61df4b05918b5648a17bf3fd8b7a7d # Parent 7b07dd104a1a5ea06e296933aa56794b90475b70 check result: Envir.beta_norm; diff -r 7b07dd104a1a -r 97d25c125c61 src/Pure/goals.ML --- a/src/Pure/goals.ML Fri Nov 17 18:50:01 2000 +0100 +++ b/src/Pure/goals.ML Fri Nov 17 18:50:52 2000 +0100 @@ -227,7 +227,7 @@ (filter (fn x => (not (Locale.in_locale [x] sign))) hyps))) else if Pattern.matches (#tsig(Sign.rep_sg sign)) - (term_of chorn, prop) + (Envir.beta_norm (term_of chorn), Envir.beta_norm prop) then final_th else !result_error_fn state "proved a different theorem" end