# HG changeset patch
# User wenzelm
# Date 965422733 -7200
# Node ID 0d14a9e7930c6f1e25ec439b8a60b042199470dc
# Parent  fb68b716396942494d76530795bf1c75a72407bb
dummy_pattern moved to term.ML;

diff -r fb68b7163969 -r 0d14a9e7930c src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Aug 04 22:58:38 2000 +0200
+++ b/src/Pure/pure_thy.ML	Fri Aug 04 22:58:53 2000 +0200
@@ -55,7 +55,6 @@
   val end_theory: theory -> theory
   val checkpoint: theory -> theory
   val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
-  val dummy_patternN: string
 end;
 
 structure PureThy: PURE_THY =
@@ -418,8 +417,6 @@
 
 (*** the ProtoPure theory ***)
 
-val dummy_patternN = "dummy_pattern";
-
 val proto_pure =
   Theory.pre_pure
   |> Library.apply [TheoremsData.init, TheoryManagementData.init]
@@ -444,7 +441,7 @@
   |> Theory.add_trfunsT Syntax.pure_trfunsT
   |> Theory.add_syntax
    [("==>", "[prop, prop] => prop", Delimfix "op ==>"),
-    (dummy_patternN, "aprop", Delimfix "'_")]
+    (Term.dummy_patternN, "aprop", Delimfix "'_")]
   |> Theory.add_consts
    [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
     ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
@@ -452,7 +449,7 @@
     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
     ("Goal", "prop => prop", Mixfix ("GOAL _", [1000], 999)),
     ("TYPE", "'a itself", NoSyn),
-    (dummy_patternN, "'a", Delimfix "'_")]
+    (Term.dummy_patternN, "'a", Delimfix "'_")]
   |> Theory.add_modesyntax ("", false)
     [("Goal", "prop => prop", Mixfix ("_", [0], 0))]
   |> local_path