1.1 --- a/src/Pure/tactic.ML	Tue Nov 13 16:12:25 2001 +0100
     1.2 +++ b/src/Pure/tactic.ML	Tue Nov 13 17:51:03 2001 +0100
     1.3 @@ -635,7 +635,7 @@
     1.4      fun err msg = error (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
     1.5        Sign.string_of_term sign (Term.list_all_free (params, statement)));
     1.6  
     1.7 -    fun cert_safe t = Thm.cterm_of sign t
     1.8 +    fun cert_safe t = Thm.cterm_of sign (Envir.beta_norm t)
     1.9        handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
    1.10  
    1.11      val _ = cert_safe statement;