dummy_patterns moved to term.ML;
authorwenzelm
Fri Aug 04 23:02:11 2000 +0200 (2000-08-04)
changeset 954002c51ca9c531
parent 9539 7ff8f3516d54
child 9541 d17c0b34d5c8
dummy_patterns moved to term.ML;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Aug 04 23:01:39 2000 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Aug 04 23:02:11 2000 +0200
     1.3 @@ -511,23 +511,10 @@
     1.4  
     1.5  (* dummy patterns *)
     1.6  
     1.7 -local
     1.8 -
     1.9 -fun is_dummy (Const (c, _)) = c = PureThy.dummy_patternN
    1.10 -  | is_dummy _ = false;
    1.11 -
    1.12 -fun prep_dummy (i, t) =
    1.13 -  if is_dummy t then (i + 1, Var (("_dummy_", i), Term.fastype_of t)) else (i, t);
    1.14 +fun prepare_dummies t = #2 (Term.replace_dummy_patterns (1, t));
    1.15  
    1.16 -in
    1.17 -
    1.18 -fun prepare_dummies tm = #2 (Term.foldl_map_aterms prep_dummy (1, tm));
    1.19 -
    1.20 -fun reject_dummies ctxt tm =
    1.21 -  if foldl_aterms (fn (ok, t) => ok andalso not (is_dummy t)) (true, tm) then tm
    1.22 -  else raise CONTEXT ("Illegal dummy pattern(s) in term", ctxt);
    1.23 -
    1.24 -end;
    1.25 +fun reject_dummies ctxt t = Term.no_dummy_patterns t
    1.26 +  handle TERM _ => raise CONTEXT ("Illegal dummy pattern(s) in term", ctxt);
    1.27  
    1.28  
    1.29  (* read terms *)