src/Pure/tactic.ML

     val params = mapfilter (fn x => apsome (pair x) (assoc_string (frees, x))) xs;
 
     fun err msg = error (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
       Sign.string_of_term sign (Term.list_all_free (params, statement)));
 
-    fun cert_safe t = Thm.cterm_of sign t
+    fun cert_safe t = Thm.cterm_of sign (Envir.beta_norm t)
       handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
 
     val _ = cert_safe statement;
     val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => err msg;