# HG changeset patch
# User wenzelm
# Date 1303064146 -7200
# Node ID c3abf2c3f541566afe9af1725c9756b8958f9bd4
# Parent  774df7c59508dd9b1f2a75273a43812987adba8a
eliminated obsolete markup -- superseded by generic "entity" markup;

diff -r 774df7c59508 -r c3abf2c3f541 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun Apr 17 19:54:04 2011 +0200
+++ b/src/Pure/General/markup.ML	Sun Apr 17 20:15:46 2011 +0200
@@ -38,12 +38,9 @@
   val tyconN: string val tycon: string -> T
   val fixed_declN: string val fixed_decl: string -> T
   val fixedN: string val fixed: string -> T
-  val const_declN: string val const_decl: string -> T
   val constN: string val const: string -> T
-  val fact_declN: string val fact_decl: string -> T
   val factN: string val fact: string -> T
   val dynamic_factN: string val dynamic_fact: string -> T
-  val local_fact_declN: string val local_fact_decl: string -> T
   val local_factN: string val local_fact: string -> T
   val tfreeN: string val tfree: T
   val tvarN: string val tvar: T
@@ -218,12 +215,9 @@
 val (tyconN, tycon) = markup_string "tycon" nameN;
 val (fixed_declN, fixed_decl) = markup_string "fixed_decl" nameN;
 val (fixedN, fixed) = markup_string "fixed" nameN;
-val (const_declN, const_decl) = markup_string "const_decl" nameN;
 val (constN, const) = markup_string "constant" nameN;
-val (fact_declN, fact_decl) = markup_string "fact_decl" nameN;
 val (factN, fact) = markup_string "fact" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
-val (local_fact_declN, local_fact_decl) = markup_string "local_fact_decl" nameN;
 val (local_factN, local_fact) = markup_string "local_fact" nameN;
 
 
diff -r 774df7c59508 -r c3abf2c3f541 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sun Apr 17 19:54:04 2011 +0200
+++ b/src/Pure/General/markup.scala	Sun Apr 17 20:15:46 2011 +0200
@@ -151,12 +151,9 @@
   val TYCON = "tycon"
   val FIXED_DECL = "fixed_decl"
   val FIXED = "fixed"
-  val CONST_DECL = "const_decl"
   val CONST = "constant"
-  val FACT_DECL = "fact_decl"
   val FACT = "fact"
   val DYNAMIC_FACT = "dynamic_fact"
-  val LOCAL_FACT_DECL = "local_fact_decl"
   val LOCAL_FACT = "local_fact"
 
 
diff -r 774df7c59508 -r c3abf2c3f541 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Apr 17 19:54:04 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Apr 17 20:15:46 2011 +0200
@@ -912,10 +912,7 @@
 
 fun note_thmss kind = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
   let
-    val pos = Binding.pos_of b;
     val name = full_name ctxt b;
-    val _ = Context_Position.report ctxt pos (Markup.local_fact_decl name);
-
     val facts = Global_Theory.name_thmss false name raw_facts;
     fun app (th, attrs) x =
       swap (Library.foldl_map
diff -r 774df7c59508 -r c3abf2c3f541 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sun Apr 17 19:54:04 2011 +0200
+++ b/src/Pure/global_theory.ML	Sun Apr 17 20:15:46 2011 +0200
@@ -185,10 +185,7 @@
 
 fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
   let
-    val pos = Binding.pos_of b;
     val name = Sign.full_name thy b;
-    val _ = Position.report pos (Markup.fact_decl name);
-
     fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
     val (thms, thy') = thy |> enter_thms
       (name_thmss true) (name_thms false true) (apsnd flat o Library.foldl_map app)
diff -r 774df7c59508 -r c3abf2c3f541 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Apr 17 19:54:04 2011 +0200
+++ b/src/Pure/sign.ML	Sun Apr 17 20:15:46 2011 +0200
@@ -419,13 +419,7 @@
 fun add_consts_i args thy =
   #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);
 
-fun declare_const ctxt ((b, T), mx) thy =
-  let
-    val pos = Binding.pos_of b;
-    val ([const as Const (c, _)], thy') = gen_add_consts (K I) ctxt [(b, T, mx)] thy;
-    val _ = Position.report pos (Markup.const_decl c);
-  in (const, thy') end;
-
+fun declare_const ctxt ((b, T), mx) = yield_singleton (gen_add_consts (K I) ctxt) (b, T, mx);
 fun declare_const_global arg thy = declare_const (Proof_Context.init_global thy) arg thy;
 
 end;
diff -r 774df7c59508 -r c3abf2c3f541 src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Apr 17 19:54:04 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Apr 17 20:15:46 2011 +0200
@@ -154,12 +154,9 @@
       Markup.TYCON -> NULL,
       Markup.FIXED_DECL -> FUNCTION,
       Markup.FIXED -> NULL,
-      Markup.CONST_DECL -> FUNCTION,
       Markup.CONST -> LITERAL2,
-      Markup.FACT_DECL -> FUNCTION,
       Markup.FACT -> NULL,
       Markup.DYNAMIC_FACT -> LABEL,
-      Markup.LOCAL_FACT_DECL -> FUNCTION,
       Markup.LOCAL_FACT -> NULL,
       // inner syntax
       Markup.TFREE -> NULL,