# HG changeset patch
# User wenzelm
# Date 1191162041 -7200
# Node ID 2949fb459c7b5b4797088a3e3d6db6d2be0ef1c8
# Parent  3e7f71caae189b5c82e19234ac28b2c2ada2f57a
keep context position as tags for consts/thms;

diff -r 3e7f71caae18 -r 2949fb459c7b src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sun Sep 30 16:20:40 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML	Sun Sep 30 16:20:41 2007 +0200
@@ -64,16 +64,17 @@
       | _ => false);
   in
     eq_heads ? (Context.mapping_result
-      (Sign.add_abbrev Syntax.internalM arg') (ProofContext.add_abbrev Syntax.internalM arg')
+      (Sign.add_abbrev Syntax.internalM [] arg') (ProofContext.add_abbrev Syntax.internalM [] arg')
     #-> (fn (lhs, _) =>
       Term.equiv_types (rhs, rhs') ?
         Morphism.form (ProofContext.target_notation prmode [(lhs, mx)])))
   end;
 
-fun internal_abbrev prmode ((c, mx), t) =
+fun internal_abbrev prmode ((c, mx), t) lthy = lthy
   (* FIXME really permissive *)
-  LocalTheory.term_syntax (perhaps o try o target_abbrev prmode ((c, mx), t))
-  #> ProofContext.add_abbrev Syntax.internalM (c, t) #> snd;
+  |> LocalTheory.term_syntax (perhaps o try o target_abbrev prmode ((c, mx), t))
+  |> ProofContext.add_abbrev Syntax.internalM (ContextPosition.properties_of lthy) (c, t)
+  |> snd;
 
 fun consts is_loc some_class depends decls lthy =
   let
@@ -84,7 +85,7 @@
         val U = map #2 xs ---> T;
         val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);
         val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx;
-        val thy' = Sign.add_consts_authentic [(c, U, mx1)] thy;
+        val thy' = Sign.add_consts_authentic (ContextPosition.properties_of lthy) [(c, U, mx1)] thy;
       in (((c, mx2), t), thy') end;
 
     fun const_class (SOME class) ((c, _), mx) (_, t) =
@@ -151,8 +152,8 @@
     val U = Term.fastype_of u;
     val u' = singleton (Variable.export_terms (Variable.declare_term u target) thy_ctxt) u;
 
-    val ((lhs as Const (full_c, _), rhs), lthy1) = lthy
-      |> LocalTheory.theory_result (Sign.add_abbrev (#1 prmode) (c, u'));
+    val ((lhs as Const (full_c, _), rhs), lthy1) = lthy |> LocalTheory.theory_result
+      (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u'));
     val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx;
   in
     lthy1
@@ -267,6 +268,7 @@
     val result = th''
       |> PureThy.name_thm true true ""
       |> Goal.close_result
+      |> fold PureThy.tag_rule (ContextPosition.properties_of ctxt)
       |> PureThy.name_thm true true name;
 
     (*import fixes*)