# HG changeset patch
# User wenzelm
# Date 1369595103 -7200
# Node ID 51eca565b153e3556d63113cf0bc1842c4c6e3a6
# Parent  7746c9f1baf332c6eb2f5b831018e3e3e10fb731
tuned;

diff -r 7746c9f1baf3 -r 51eca565b153 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sun May 26 20:42:43 2013 +0200
+++ b/src/Pure/pure_thy.ML	Sun May 26 21:05:03 2013 +0200
@@ -164,7 +164,7 @@
     ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
     ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
     (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
-    (const Term.dummy_patternN, typ "aprop",           Delimfix "'_"),
+    (const "dummy_pattern", typ "aprop",               Delimfix "'_"),
     ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
     (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
     (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
@@ -194,12 +194,12 @@
     (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
     (Binding.name "prop", typ "prop => prop", NoSyn),
     (Binding.name "TYPE", typ "'a itself", NoSyn),
-    (Binding.name Term.dummy_patternN, typ "'a", Delimfix "'_")]
+    (Binding.name "dummy_pattern", typ "'a", Delimfix "'_")]
   #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
   #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
   #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
   #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
-  #> Theory.add_deps_global Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
+  #> Theory.add_deps_global "dummy_pattern" ("dummy_pattern", typ "'a") []
   #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
   #> Sign.parse_translation Syntax_Trans.pure_parse_translation
   #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
diff -r 7746c9f1baf3 -r 51eca565b153 src/Pure/term.ML
--- a/src/Pure/term.ML	Sun May 26 20:42:43 2013 +0200
+++ b/src/Pure/term.ML	Sun May 26 21:05:03 2013 +0200
@@ -159,7 +159,6 @@
   val maxidx_term: term -> int -> int
   val has_abs: term -> bool
   val dest_abs: string * typ * term -> string * term
-  val dummy_patternN: string
   val dummy_pattern: typ -> term
   val dummy: term
   val dummy_prop: term
@@ -925,9 +924,7 @@
 
 (* dummy patterns *)
 
-val dummy_patternN = "dummy_pattern";
-
-fun dummy_pattern T = Const (dummy_patternN, T);
+fun dummy_pattern T = Const ("dummy_pattern", T);
 val dummy = dummy_pattern dummyT;
 val dummy_prop = dummy_pattern propT;
 
diff -r 7746c9f1baf3 -r 51eca565b153 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sun May 26 20:42:43 2013 +0200
+++ b/src/Tools/Code/code_target.ML	Sun May 26 21:05:03 2013 +0200
@@ -419,7 +419,7 @@
     val value_name = "Value.value.value"
     val program = prepared_program
       |> Graph.new_node (value_name,
-          Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
+          Code_Thingol.Fun (@{const_name dummy_pattern}, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
       |> fold (curry (perhaps o try o Graph.add_edge) value_name) consts;
     val (program_code, deresolve) = produce (mounted_serializer program);
     val value_name' = the (deresolve value_name);
diff -r 7746c9f1baf3 -r 51eca565b153 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sun May 26 20:42:43 2013 +0200
+++ b/src/Tools/Code/code_thingol.ML	Sun May 26 21:05:03 2013 +0200
@@ -938,24 +938,24 @@
     val ty = fastype_of t;
     val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
       o dest_TFree))) t [];
-    val t' = annotate thy algbr eqngr (Term.dummy_patternN, ty) [] t;
+    val t' = annotate thy algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
     val stmt_value =
       fold_map (translate_tyvar_sort thy algbr eqngr false) vs
       ##>> translate_typ thy algbr eqngr false ty
       ##>> translate_term thy algbr eqngr false NONE (t', NONE)
       #>> (fn ((vs, ty), t) => Fun
-        (Term.dummy_patternN, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
+        (@{const_name dummy_pattern}, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
     fun term_value (dep, (naming, program1)) =
       let
         val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
-          Graph.get_node program1 Term.dummy_patternN;
-        val deps = Graph.immediate_succs program1 Term.dummy_patternN;
-        val program2 = Graph.del_node Term.dummy_patternN program1;
+          Graph.get_node program1 @{const_name dummy_pattern};
+        val deps = Graph.immediate_succs program1 @{const_name dummy_pattern};
+        val program2 = Graph.del_node @{const_name dummy_pattern} program1;
         val deps_all = Graph.all_succs program2 deps;
         val program3 = Graph.restrict (member (op =) deps_all) program2;
       in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
   in
-    ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN
+    ensure_stmt ((K o K) NONE) pair stmt_value @{const_name dummy_pattern}
     #> snd
     #> term_value
   end;