# HG changeset patch
# User wenzelm
# Date 965422718 -7200
# Node ID fb68b716396942494d76530795bf1c75a72407bb
# Parent  36b9bc6eb4540a3be91b3bf82815ed896f0f6202
Term.no_dummy_patterns;

diff -r 36b9bc6eb454 -r fb68b7163969 src/Pure/goals.ML
--- 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;