src/Pure/codegen.ML
changeset 27398 768da1da59d6
parent 27353 71c4dd53d4cb
child 27724 0cc30a837f26
     1.1 --- a/src/Pure/codegen.ML	Mon Jun 30 13:41:31 2008 +0200
     1.2 +++ b/src/Pure/codegen.ML	Mon Jun 30 13:41:33 2008 +0200
     1.3 @@ -57,8 +57,8 @@
     1.4    val get_const_id: string -> codegr -> string * string
     1.5    val mk_type_id: string -> string -> codegr -> codegr * (string * string)
     1.6    val get_type_id: string -> codegr -> string * string
     1.7 -  val thyname_of_type: string -> theory -> string
     1.8 -  val thyname_of_const: string -> theory -> string
     1.9 +  val thyname_of_type: theory -> string -> string
    1.10 +  val thyname_of_const: theory -> string -> string
    1.11    val rename_terms: term list -> term list
    1.12    val rename_term: term -> term
    1.13    val new_names: term -> string list -> string list
    1.14 @@ -496,23 +496,13 @@
    1.15  fun map_node k f (gr, x) = (Graph.map_node k f gr, x);
    1.16  fun new_node p (gr, x) = (Graph.new_node p gr, x);
    1.17  
    1.18 -fun theory_of_type s thy =
    1.19 -  if Sign.declared_tyname thy s
    1.20 -  then SOME (the_default thy (get_first (theory_of_type s) (Theory.parents_of thy)))
    1.21 -  else NONE;
    1.22 +fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN);
    1.23  
    1.24 -fun theory_of_const s thy =
    1.25 -  if Sign.declared_const thy s
    1.26 -  then SOME (the_default thy (get_first (theory_of_const s) (Theory.parents_of thy)))
    1.27 -  else NONE;
    1.28 +fun thyname_of_type thy =
    1.29 +  thyname_of thy (Type.the_tags (Sign.tsig_of thy));
    1.30  
    1.31 -fun thyname_of_type s thy = (case theory_of_type s thy of
    1.32 -    NONE => error ("thyname_of_type: no such type: " ^ quote s)
    1.33 -  | SOME thy' => Context.theory_name thy');
    1.34 -
    1.35 -fun thyname_of_const s thy = (case theory_of_const s thy of
    1.36 -    NONE => error ("thyname_of_const: no such constant: " ^ quote s)
    1.37 -  | SOME thy' => Context.theory_name thy');
    1.38 +fun thyname_of_const thy =
    1.39 +  thyname_of thy (Consts.the_tags (Sign.consts_of thy));
    1.40  
    1.41  fun rename_terms ts =
    1.42    let
    1.43 @@ -695,7 +685,7 @@
    1.44                   val (gr4, _) = invoke_tycodegen thy defs dep module false
    1.45                     (gr3, funpow (length ts) (hd o tl o snd o dest_Type) T);
    1.46                   val (module', suffix) = (case get_defn thy defs s T of
    1.47 -                     NONE => (if_library (thyname_of_const s thy) module, "")
    1.48 +                     NONE => (if_library (thyname_of_const thy s) module, "")
    1.49                     | SOME ((U, (module', _)), NONE) =>
    1.50                         (if_library module' module, "")
    1.51                     | SOME ((U, (module', _)), SOME i) =>
    1.52 @@ -780,7 +770,7 @@
    1.53               val (gr'', qs) = foldl_map
    1.54                 (invoke_tycodegen thy defs dep module false)
    1.55                 (gr', quotes_of ms);
    1.56 -             val module' = if_library (thyname_of_type s thy) module;
    1.57 +             val module' = if_library (thyname_of_type thy s) module;
    1.58               val node_id = s ^ " (type)";
    1.59               fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs)
    1.60             in SOME (case try (get_node gr'') node_id of