renamed 'dummy' to 'dummy_pattern' (less dangerous);
authorwenzelm
Sat May 01 00:10:05 1999 +0200 (1999-05-01)
changeset 65601436349f8b28
parent 6559 fa203026941c
child 6561 793b33191ce3
renamed 'dummy' to 'dummy_pattern' (less dangerous);
src/Pure/Isar/proof_context.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Apr 30 18:25:10 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sat May 01 00:10:05 1999 +0200
     1.3 @@ -382,7 +382,7 @@
     1.4  
     1.5  (* dummy patterns *)
     1.6  
     1.7 -fun is_dummy (Const ("dummy", _)) = true
     1.8 +fun is_dummy (Const (c, _)) = c = PureThy.dummy_patternN
     1.9    | is_dummy _ = false;
    1.10  
    1.11  fun reject_dummies ctxt tm =
    1.12 @@ -390,8 +390,8 @@
    1.13    else raise CONTEXT ("Illegal dummy pattern(s) in term", ctxt);
    1.14  
    1.15  
    1.16 -fun prep_dummy (i, Const ("dummy", T)) = (i + 1, Var (("_dummy_", i), T))
    1.17 -  | prep_dummy i_t = i_t;
    1.18 +fun prep_dummy (i, t) =
    1.19 +  if is_dummy t then (i + 1, Var (("_dummy_", i), Term.fastype_of t)) else (i, t);
    1.20  
    1.21  fun prepare_dummies tm = #2 (Term.foldl_map_aterms prep_dummy (1, tm));
    1.22  
     2.1 --- a/src/Pure/pure_thy.ML	Fri Apr 30 18:25:10 1999 +0200
     2.2 +++ b/src/Pure/pure_thy.ML	Sat May 01 00:10:05 1999 +0200
     2.3 @@ -51,6 +51,7 @@
     2.4    exception ROLLBACK of theory * exn option
     2.5    val transaction: (theory -> theory) -> theory -> theory
     2.6    val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
     2.7 +  val dummy_patternN: string
     2.8  end;
     2.9  
    2.10  structure PureThy: PURE_THY =
    2.11 @@ -407,6 +408,8 @@
    2.12  
    2.13  (*** the ProtoPure theory ***)
    2.14  
    2.15 +val dummy_patternN = "dummy_pattern";
    2.16 +
    2.17  val proto_pure =
    2.18    Theory.pre_pure
    2.19    |> Library.apply [TheoremsData.init, TheoryManagementData.init]
    2.20 @@ -438,7 +441,7 @@
    2.21      ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
    2.22      ("Goal", "prop => prop", Mixfix ("GOAL _", [999], 1000)),
    2.23      ("TYPE", "'a itself", NoSyn),
    2.24 -    ("dummy", "'a", Delimfix "'_")]
    2.25 +    (dummy_patternN, "'a", Delimfix "'_")]
    2.26    |> Theory.add_modesyntax ("", false)
    2.27      [("Goal", "prop => prop", Mixfix ("_", [0], 0))]
    2.28    |> local_path