# HG changeset patch
# User wenzelm
# Date 1256500461 -3600
# Node ID 61ee96bc989550bdabbda0144b8b64c6e21b1cdf
# Parent  292970b42770b6767cd918faab295be3d9c304be
maintain theory name via name space, not tags;
AxClass.thynames_of_arity: explicit theory name, not tags;

diff -r 292970b42770 -r 61ee96bc9895 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun Oct 25 19:21:34 2009 +0100
+++ b/src/Pure/General/markup.ML	Sun Oct 25 20:54:21 2009 +0100
@@ -13,7 +13,6 @@
   val nameN: string
   val name: string -> T -> T
   val bindingN: string val binding: string -> T
-  val theory_nameN: string
   val kindN: string
   val internalK: string
   val entityN: string val entity: string -> T
@@ -150,8 +149,6 @@
 
 val (bindingN, binding) = markup_string "binding" nameN;
 
-val theory_nameN = "theory_name";
-
 
 (* kind *)
 
diff -r 292970b42770 -r 61ee96bc9895 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun Oct 25 19:21:34 2009 +0100
+++ b/src/Pure/axclass.ML	Sun Oct 25 20:54:21 2009 +0100
@@ -36,7 +36,7 @@
   val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option
   val param_of_inst: theory -> string * string -> string
   val inst_of_param: theory -> string -> (string * string) option
-  val arity_property: theory -> class * string -> string -> string list
+  val thynames_of_arity: theory -> class * string -> string list
   type cache
   val of_sort: theory -> typ * sort -> cache -> thm list * cache  (*exception Sorts.CLASS_ERROR*)
   val cache: cache
@@ -92,8 +92,8 @@
 val arity_prefix = "arity_";
 
 type instances =
-  ((class * class) * thm) list *
-  ((class * sort list) * thm) list Symtab.table;
+  ((class * class) * thm) list *  (*classrel theorems*)
+  ((class * sort list) * (thm * string)) list Symtab.table;  (*arity theorems with theory name*)
 
 fun merge_instances ((classrel1, arities1): instances, (classrel2, arities2)) =
  (merge (eq_fst op =) (classrel1, classrel2),
@@ -175,35 +175,32 @@
 
 fun the_arity thy a (c, Ss) =
   (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss) of
-    SOME th => Thm.transfer thy th
+    SOME (th, _) => Thm.transfer thy th
   | NONE => error ("Unproven type arity " ^
       Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
 
-fun arity_property thy (c, a) x =
-  Symtab.lookup_list (snd (get_instances thy)) a
-  |> map_filter (fn ((c', _), th) => if c = c'
-      then AList.lookup (op =) (Thm.get_tags th) x else NONE)
+fun thynames_of_arity thy (c, a) =
+  Symtab.lookup_list (#2 (get_instances thy)) a
+  |> map_filter (fn ((c', _), (_, name)) => if c = c' then SOME name else NONE)
   |> rev;
 
-fun insert_arity_completions thy (t, ((c, Ss), th)) arities =
+fun insert_arity_completions thy (t, ((c, Ss), (th, thy_name))) arities =
   let
     val algebra = Sign.classes_of thy;
-    val super_class_completions = Sign.super_classes thy c
+    val super_class_completions =
+      Sign.super_classes thy c
       |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
-          andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t))
-    val tags = Thm.get_tags th;
+          andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t));
     val completions = map (fn c1 => (Sorts.weaken algebra
       (fn (th, c2) => fn c3 => th RS the_classrel thy (c2, c3)) (th, c) c1
-        |> Thm.map_tags (K tags) |> Thm.close_derivation, c1)) super_class_completions;
-    val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), th1)))
+        |> Thm.close_derivation, c1)) super_class_completions;
+    val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), (th1, thy_name))))
       completions arities;
-  in (completions, arities') end;
+  in (null completions, arities') end;
 
 fun put_arity ((t, Ss, c), th) thy =
   let
-    val th' = (Thm.map_tags o AList.default (op =))
-      (Markup.theory_nameN, Context.theory_name thy) th;
-    val arity' = (t, ((c, Ss), th'));
+    val arity' = (t, ((c, Ss), (th, Context.theory_name thy)));
   in
     thy
     |> map_instances (fn (classrel, arities) => (classrel,
@@ -216,11 +213,10 @@
 fun complete_arities thy =
   let
     val arities = snd (get_instances thy);
-    val (completions, arities') = arities
-      |> fold_map (insert_arity_completions thy) (Symtab.dest_list arities)
-      |>> flat;
-  in if null completions
-    then NONE
+    val (finished, arities') = arities
+      |> fold_map (insert_arity_completions thy) (Symtab.dest_list arities);
+  in
+    if forall I finished then NONE
     else SOME (thy |> map_instances (fn (classrel, _) => (classrel, arities')))
   end;
 
diff -r 292970b42770 -r 61ee96bc9895 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sun Oct 25 19:21:34 2009 +0100
+++ b/src/Pure/codegen.ML	Sun Oct 25 20:54:21 2009 +0100
@@ -446,13 +446,8 @@
 fun map_node k f (gr, x) = (Graph.map_node k f gr, x);
 fun new_node p (gr, x) = (Graph.new_node p gr, x);
 
-fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN);
-
-fun thyname_of_type thy =
-  thyname_of thy (Type.the_tags (Sign.tsig_of thy));
-
-fun thyname_of_const thy =
-  thyname_of thy (Consts.the_tags (Sign.consts_of thy));
+fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
+fun thyname_of_const thy = #theory_name o Name_Space.the_entry (Sign.const_space thy);
 
 fun rename_terms ts =
   let
diff -r 292970b42770 -r 61ee96bc9895 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Oct 25 19:21:34 2009 +0100
+++ b/src/Pure/sign.ML	Sun Oct 25 20:54:21 2009 +0100
@@ -434,8 +434,7 @@
   let
     val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn;
     val decls = map (fn (a, n, mx) => (Binding.map_name (Syntax.type_name mx) a, n)) types;
-    val tags = [(Markup.theory_nameN, Context.theory_name thy)];
-    val tsig' = fold (Type.add_type naming tags) decls tsig;
+    val tsig' = fold (Type.add_type naming []) decls tsig;
   in (naming, syn', tsig', consts) end);
 
 
@@ -511,10 +510,9 @@
         val T' = Logic.varifyT T;
       in ((b, T'), (c_syn, T', mx), Const (c, T)) end;
     val args = map prep raw_args;
-    val tags' = tags |> Properties.put (Markup.theory_nameN, Context.theory_name thy);
   in
     thy
-    |> map_consts (fold (Consts.declare authentic (naming_of thy) tags' o #1) args)
+    |> map_consts (fold (Consts.declare authentic (naming_of thy) tags o #1) args)
     |> add_syntax_i (map #2 args)
     |> pair (map #3 args)
   end;
diff -r 292970b42770 -r 61ee96bc9895 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sun Oct 25 19:21:34 2009 +0100
+++ b/src/Tools/Code/code_thingol.ML	Sun Oct 25 20:54:21 2009 +0100
@@ -252,19 +252,15 @@
 (* policies *)
 
 local
-  fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN);
-  fun thyname_of_class thy =
-    thyname_of thy (ProofContext.query_class (ProofContext.init thy));
-  fun thyname_of_tyco thy =
-    thyname_of thy (Type.the_tags (Sign.tsig_of thy));
-  fun thyname_of_instance thy inst = case AxClass.arity_property thy inst Markup.theory_nameN
-   of [] => error ("no such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
+  fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
+  fun thyname_of_instance thy inst = case AxClass.thynames_of_arity thy inst
+   of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
     | thyname :: _ => thyname;
   fun thyname_of_const thy c = case AxClass.class_of_param thy c
    of SOME class => thyname_of_class thy class
     | NONE => (case Code.get_datatype_of_constr thy c
-       of SOME dtco => thyname_of_tyco thy dtco
-        | NONE => thyname_of thy (Consts.the_tags (Sign.consts_of thy)) c);
+       of SOME dtco => Codegen.thyname_of_type thy dtco
+        | NONE => Codegen.thyname_of_const thy c);
   fun purify_base "op &" = "and"
     | purify_base "op |" = "or"
     | purify_base "op -->" = "implies"
@@ -282,10 +278,11 @@
 
 fun namify_class thy = namify thy Long_Name.base_name thyname_of_class;
 fun namify_classrel thy = namify thy (fn (class1, class2) => 
-  Long_Name.base_name class2 ^ "_" ^ Long_Name.base_name class1) (fn thy => thyname_of_class thy o fst);
+    Long_Name.base_name class2 ^ "_" ^ Long_Name.base_name class1)
+  (fn thy => thyname_of_class thy o fst);
   (*order fits nicely with composed projections*)
 fun namify_tyco thy "fun" = "Pure.fun"
-  | namify_tyco thy tyco = namify thy Long_Name.base_name thyname_of_tyco tyco;
+  | namify_tyco thy tyco = namify thy Long_Name.base_name Codegen.thyname_of_type tyco;
 fun namify_instance thy = namify thy (fn (class, tyco) => 
   Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance;
 fun namify_const thy = namify thy Long_Name.base_name thyname_of_const;