Term.no_dummy_patterns;

--- a/src/Pure/goals.ML	Fri Aug 04 22:58:23 2000 +0200
+++ b/src/Pure/goals.ML	Fri Aug 04 22:58:38 2000 +0200
@@ -193,6 +193,7 @@
 *)
 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;