src/Pure/goals.ML

   "atomic" indicates if the goal should be wrapped up in the function
   "Goal::prop=>prop" to avoid assumptions being returned separately.
 *)
 fun prepare_proof atomic rths chorn =
   let val {sign, t=horn,...} = rep_cterm chorn;
+      val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
       val (_,As,B) = Logic.strip_horn(horn);
       val atoms = atomic andalso
             forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As;
       val (As,B) = if atoms then ([],horn) else (As,B);
       val cAs = map (cterm_of sign) As;