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