# HG changeset patch
# User wenzelm
# Date 965422931 -7200
# Node ID 02c51ca9c5310cd6a612ffe6d82516f96d569854
# Parent  7ff8f3516d542e7872b8384a18e7866eaf540029
dummy_patterns moved to term.ML;

diff -r 7ff8f3516d54 -r 02c51ca9c531 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Aug 04 23:01:39 2000 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Aug 04 23:02:11 2000 +0200
@@ -511,23 +511,10 @@
 
 (* dummy patterns *)
 
-local
-
-fun is_dummy (Const (c, _)) = c = PureThy.dummy_patternN
-  | is_dummy _ = false;
-
-fun prep_dummy (i, t) =
-  if is_dummy t then (i + 1, Var (("_dummy_", i), Term.fastype_of t)) else (i, t);
+fun prepare_dummies t = #2 (Term.replace_dummy_patterns (1, t));
 
-in
-
-fun prepare_dummies tm = #2 (Term.foldl_map_aterms prep_dummy (1, tm));
-
-fun reject_dummies ctxt tm =
-  if foldl_aterms (fn (ok, t) => ok andalso not (is_dummy t)) (true, tm) then tm
-  else raise CONTEXT ("Illegal dummy pattern(s) in term", ctxt);
-
-end;
+fun reject_dummies ctxt t = Term.no_dummy_patterns t
+  handle TERM _ => raise CONTEXT ("Illegal dummy pattern(s) in term", ctxt);
 
 
 (* read terms *)