--- a/src/Pure/Isar/proof_context.ML Fri Apr 30 18:25:10 1999 +0200
+++ b/src/Pure/Isar/proof_context.ML Sat May 01 00:10:05 1999 +0200
@@ -382,7 +382,7 @@
(* dummy patterns *)
-fun is_dummy (Const ("dummy", _)) = true
+fun is_dummy (Const (c, _)) = c = PureThy.dummy_patternN
| is_dummy _ = false;
fun reject_dummies ctxt tm =
@@ -390,8 +390,8 @@
else raise CONTEXT ("Illegal dummy pattern(s) in term", ctxt);
-fun prep_dummy (i, Const ("dummy", T)) = (i + 1, Var (("_dummy_", i), T))
- | prep_dummy i_t = i_t;
+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 tm = #2 (Term.foldl_map_aterms prep_dummy (1, tm));
--- a/src/Pure/pure_thy.ML Fri Apr 30 18:25:10 1999 +0200
+++ b/src/Pure/pure_thy.ML Sat May 01 00:10:05 1999 +0200
@@ -51,6 +51,7 @@
exception ROLLBACK of theory * exn option
val transaction: (theory -> theory) -> theory -> theory
val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
+ val dummy_patternN: string
end;
structure PureThy: PURE_THY =
@@ -407,6 +408,8 @@
(*** the ProtoPure theory ***)
+val dummy_patternN = "dummy_pattern";
+
val proto_pure =
Theory.pre_pure
|> Library.apply [TheoremsData.init, TheoryManagementData.init]
@@ -438,7 +441,7 @@
("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
("Goal", "prop => prop", Mixfix ("GOAL _", [999], 1000)),
("TYPE", "'a itself", NoSyn),
- ("dummy", "'a", Delimfix "'_")]
+ (dummy_patternN, "'a", Delimfix "'_")]
|> Theory.add_modesyntax ("", false)
[("Goal", "prop => prop", Mixfix ("_", [0], 0))]
|> local_path