dummy patterns;
authorwenzelm
Fri Apr 30 18:05:55 1999 +0200 (1999-04-30)
changeset 655068f950b1a664
parent 6549 90fa592f6e6e
child 6551 de4047b03017
dummy patterns;
theory data: copy;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Apr 30 18:04:42 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Apr 30 18:05:55 1999 +0200
     1.3 @@ -213,6 +213,7 @@
     1.4    type T = (Object.kind * ((theory -> Object.T) * (context -> Object.T -> unit))) Symtab.table;
     1.5  
     1.6    val empty = Symtab.empty;
     1.7 +  val copy = I;
     1.8    val prep_ext = I;
     1.9    fun merge tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs
    1.10      handle Symtab.DUPS kinds => err_inconsistent kinds;
    1.11 @@ -379,6 +380,22 @@
    1.12    in normh end;
    1.13  
    1.14  
    1.15 +(* dummy patterns *)
    1.16 +
    1.17 +fun is_dummy (Const ("dummy", _)) = true
    1.18 +  | is_dummy _ = false;
    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 +
    1.25 +fun prep_dummy (i, Const ("dummy", T)) = (i + 1, Var (("_dummy_", i), T))
    1.26 +  | prep_dummy i_t = i_t;
    1.27 +
    1.28 +fun prepare_dummies tm = #2 (Term.foldl_map_aterms prep_dummy (1, tm));
    1.29 +
    1.30 +
    1.31  (* read terms *)
    1.32  
    1.33  fun gen_read read app is_pat (ctxt as Context {binds, defs = (types, sorts, _, used), ...}) s =
    1.34 @@ -397,6 +414,7 @@
    1.35        | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
    1.36      |> app (intern_skolem ctxt true)
    1.37      |> app (if is_pat then I else norm_term ctxt)
    1.38 +    |> app (if is_pat then prepare_dummies else (reject_dummies ctxt))
    1.39    end;
    1.40  
    1.41  val read_termTs = gen_read (read_def_termTs false) (apfst o map) false;