src/Tools/code/code_thingol.ML

   val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
   val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
   val is_cons: program -> string -> bool
   val contr_classparam_typs: program -> string -> itype option list
 
+  val read_const_exprs: theory -> string list -> string list * string list
   val consts_program: theory -> string list -> string list * (naming * program)
   val cached_program: theory -> naming * program
   val eval_conv: theory -> (sort -> sort)
     -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> cterm -> thm)
     -> cterm -> thm

   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);
+  fun purify_base "op &" = "and"
+    | purify_base "op |" = "or"
+    | purify_base "op -->" = "implies"
+    | purify_base "op :" = "member"
+    | purify_base "op =" = "eq"
+    | purify_base "*" = "product"
+    | purify_base "+" = "sum"
+    | purify_base s = Name.desymbolize false s;
   fun namify thy get_basename get_thyname name =
     let
       val prefix = get_thyname thy name;
-      val base = (Code_Name.purify_base o get_basename) name;
+      val base = (purify_base o get_basename) name;
     in Long_Name.append prefix base end;
 in
 
 fun namify_class thy = namify thy Long_Name.base_name thyname_of_class;
 fun namify_classrel thy = namify thy (fn (class1, class2) => 

 fun eval thy prep_sort postproc = Code_Wellsorted.eval thy prep_sort postproc o base_evaluator thy;
 
 
 (** diagnostic commands **)
 
+fun read_const_exprs thy =
+  let
+    fun consts_of some_thyname =
+      let
+        val thy' = case some_thyname
+         of SOME thyname => ThyInfo.the_theory thyname thy
+          | NONE => thy;
+        val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
+          ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
+        fun belongs_here c =
+          not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
+      in case some_thyname
+       of NONE => cs
+        | SOME thyname => filter belongs_here cs
+      end;
+    fun read_const_expr "*" = ([], consts_of NONE)
+      | read_const_expr s = if String.isSuffix ".*" s
+          then ([], consts_of (SOME (unsuffix ".*" s)))
+          else ([Code_Unit.read_const thy s], []);
+  in pairself flat o split_list o map read_const_expr end;
+
 fun code_depgr thy consts =
   let
     val (_, eqngr) = Code_Wellsorted.obtain thy consts [];
     val select = Graph.all_succs eqngr consts;
   in

 local
 
 structure P = OuterParse
 and K = OuterKeyword
 
-fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
-fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
+fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy;
+fun code_deps_cmd thy = code_deps thy o op @ o read_const_exprs thy;
 
 in
 
 val _ =
   OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag