# HG changeset patch
# User haftmann
# Date 1214826093 -7200
# Node ID 768da1da59d67299b27171af359cd6dd410a104f
# Parent  1d8456c5d53d1b4fcf28dda24a10ddac59254d9e
simplified retrieval of theory names of consts and types

diff -r 1d8456c5d53d -r 768da1da59d6 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Mon Jun 30 13:41:31 2008 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Mon Jun 30 13:41:33 2008 +0200
@@ -46,7 +46,7 @@
 
     val (_, (tname, _, _)) :: _ = descr';
     val node_id = tname ^ " (type)";
-    val module' = if_library (thyname_of_type tname thy) module;
+    val module' = if_library (thyname_of_type thy tname) module;
 
     fun mk_dtdef gr prfx [] = (gr, [])
       | mk_dtdef gr prfx ((_, (tname, dts, cs))::xs) =
diff -r 1d8456c5d53d -r 768da1da59d6 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Mon Jun 30 13:41:31 2008 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon Jun 30 13:41:33 2008 +0200
@@ -48,7 +48,7 @@
   let
     val {intros, graph, eqns} = CodegenData.get thy;
     fun thyname_of s = (case optmod of
-      NONE => thyname_of_const s thy | SOME s => s);
+      NONE => Codegen.thyname_of_const thy s | SOME s => s);
   in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of
       SOME (Const ("op =", _), [t, _]) => (case head_of t of
         Const (s, _) =>
@@ -85,7 +85,7 @@
       NONE => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of
         NONE => NONE
       | SOME ({names, ...}, {intrs, raw_induct, ...}) =>
-          SOME (names, thyname_of_const s thy,
+          SOME (names, Codegen.thyname_of_const thy s,
             length (InductivePackage.params_of raw_induct),
             preprocess thy intrs))
     | SOME _ =>
diff -r 1d8456c5d53d -r 768da1da59d6 src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Mon Jun 30 13:41:31 2008 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Mon Jun 30 13:41:33 2008 +0200
@@ -73,7 +73,7 @@
          else (preprocess thy (map fst thms'),
            case snd (snd (split_last thms')) of
                NONE => (case get_defn thy defs s T of
-                   NONE => thyname_of_const s thy
+                   NONE => Codegen.thyname_of_const thy s
                  | SOME ((_, (thyname, _)), _) => thyname)
              | SOME thyname => thyname)
        end);
diff -r 1d8456c5d53d -r 768da1da59d6 src/HOL/Tools/typedef_codegen.ML
--- a/src/HOL/Tools/typedef_codegen.ML	Mon Jun 30 13:41:31 2008 +0200
+++ b/src/HOL/Tools/typedef_codegen.ML	Mon Jun 30 13:41:33 2008 +0200
@@ -52,7 +52,7 @@
            if is_some (Codegen.get_assoc_type thy tname) then NONE else
            let
              val module' = Codegen.if_library
-               (Codegen.thyname_of_type tname thy) module;
+               (Codegen.thyname_of_type thy tname) module;
              val node_id = tname ^ " (type)";
              val (gr', (((qs, (_, Abs_id)), (_, Rep_id)), ty_id)) = foldl_map
                  (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
diff -r 1d8456c5d53d -r 768da1da59d6 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Mon Jun 30 13:41:31 2008 +0200
+++ b/src/Pure/codegen.ML	Mon Jun 30 13:41:33 2008 +0200
@@ -57,8 +57,8 @@
   val get_const_id: string -> codegr -> string * string
   val mk_type_id: string -> string -> codegr -> codegr * (string * string)
   val get_type_id: string -> codegr -> string * string
-  val thyname_of_type: string -> theory -> string
-  val thyname_of_const: string -> theory -> string
+  val thyname_of_type: theory -> string -> string
+  val thyname_of_const: theory -> string -> string
   val rename_terms: term list -> term list
   val rename_term: term -> term
   val new_names: term -> string list -> string list
@@ -496,23 +496,13 @@
 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 theory_of_type s thy =
-  if Sign.declared_tyname thy s
-  then SOME (the_default thy (get_first (theory_of_type s) (Theory.parents_of thy)))
-  else NONE;
+fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN);
 
-fun theory_of_const s thy =
-  if Sign.declared_const thy s
-  then SOME (the_default thy (get_first (theory_of_const s) (Theory.parents_of thy)))
-  else NONE;
+fun thyname_of_type thy =
+  thyname_of thy (Type.the_tags (Sign.tsig_of thy));
 
-fun thyname_of_type s thy = (case theory_of_type s thy of
-    NONE => error ("thyname_of_type: no such type: " ^ quote s)
-  | SOME thy' => Context.theory_name thy');
-
-fun thyname_of_const s thy = (case theory_of_const s thy of
-    NONE => error ("thyname_of_const: no such constant: " ^ quote s)
-  | SOME thy' => Context.theory_name thy');
+fun thyname_of_const thy =
+  thyname_of thy (Consts.the_tags (Sign.consts_of thy));
 
 fun rename_terms ts =
   let
@@ -695,7 +685,7 @@
                  val (gr4, _) = invoke_tycodegen thy defs dep module false
                    (gr3, funpow (length ts) (hd o tl o snd o dest_Type) T);
                  val (module', suffix) = (case get_defn thy defs s T of
-                     NONE => (if_library (thyname_of_const s thy) module, "")
+                     NONE => (if_library (thyname_of_const thy s) module, "")
                    | SOME ((U, (module', _)), NONE) =>
                        (if_library module' module, "")
                    | SOME ((U, (module', _)), SOME i) =>
@@ -780,7 +770,7 @@
              val (gr'', qs) = foldl_map
                (invoke_tycodegen thy defs dep module false)
                (gr', quotes_of ms);
-             val module' = if_library (thyname_of_type s thy) module;
+             val module' = if_library (thyname_of_type thy s) module;
              val node_id = s ^ " (type)";
              fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs)
            in SOME (case try (get_node gr'') node_id of