src/Pure/tactic.ML

   let
     val statement = Logic.list_implies (asms, prop);
     val frees = map Term.dest_Free (Term.term_frees statement);
     val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
     val fixed_tfrees = foldr Term.add_typ_tfree_names (map #2 fixed_frees, []);
-
     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
       handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
 
     val _ = cert_safe statement;
-    val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => error msg;
-
+    val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => err msg;
+
+    val cparams = map (cert_safe o Free) params;
     val casms = map cert_safe asms;
     val prems = map (norm_hhf o Thm.assume) casms;
     val goal = Drule.mk_triv_goal (cert_safe prop);
 
     val goal' =

     else if not (Pattern.matches (Sign.tsig_of sign) (prop, prop')) then
       err ("Proved a different theorem: " ^ Sign.string_of_term sign prop')
     else
       raw_result
       |> Drule.implies_intr_list casms
-      |> Drule.forall_intr_list (map (cert_safe o Free) params)
+      |> Drule.forall_intr_list cparams
       |> norm_hhf
       |> Thm.varifyT' fixed_tfrees
       |> Drule.zero_var_indexes
   end;