# HG changeset patch
# User wenzelm
# Date 925510205 -7200
# Node ID 1436349f8b284dd744a790063f340e38e22f93a7
# Parent  fa203026941c8782ec79909aa893aa751bafce45
renamed 'dummy' to 'dummy_pattern' (less dangerous);

diff -r fa203026941c -r 1436349f8b28 src/Pure/Isar/proof_context.ML
--- 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));
 
diff -r fa203026941c -r 1436349f8b28 src/Pure/pure_thy.ML
--- 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