src/Tools/code/code_package.ML

   in (("codevals", code''), (ctxt', args')) end;
 
 
 (* const expressions *)
 
+local
+
+fun consts_of thy some_thyname =
+  let
+    val this_thy = Option.map ThyInfo.get_theory some_thyname |> the_default thy;
+    val raw_cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
+      ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) [];
+    val cs = map (CodeUnit.subst_alias thy) raw_cs;
+    fun belongs_here thyname c =
+      not (exists (fn thy' => Sign.declared_const thy' c) (Theory.parents_of this_thy))
+  in case some_thyname
+   of NONE => cs
+    | SOME thyname => filter (belongs_here thyname) cs
+  end;
+
+fun read_const_expr thy "*" = ([], consts_of thy NONE)
+  | read_const_expr thy s = if String.isSuffix ".*" s
+      then ([], consts_of thy (SOME (unsuffix ".*" s)))
+      else ([CodeUnit.read_const thy s], []);
+
+in
+
+fun read_const_exprs thy select exprs =
+  case (pairself flat o split_list o map (read_const_expr thy)) exprs
+   of (consts, []) => (false, consts)
+    | (consts, consts') => (true, consts @ select consts');
+
+end; (*local*)
+
 fun filter_generatable thy consts =
   let
     val (consts', funcgr) = CodeFuncgr.make_consts thy consts;
     val (consts'', _) = generate thy funcgr (fold_map ooo perhaps_const) consts';
     val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE)
       (consts' ~~ consts'');
   in consts''' end;
 
 fun generate_const_exprs thy raw_cs =
   let
-    val (perm1, cs) = CodeUnit.read_const_exprs thy
+    val (perm1, cs) = read_const_exprs thy
       (filter_generatable thy) raw_cs;
     val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs)
       (fold_map ooo ensure_const) cs
      of ([], _) => (true, NONE)
       | (cs, _) => (false, SOME cs);

     val (permissive, cs) = generate_const_exprs thy raw_cs;
     val _ = code thy permissive cs seris;
   in () end;
 
 fun code_thms_cmd thy =
-  code_thms thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
+  code_thms thy o snd o read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
 
 fun code_deps_cmd thy =
-  code_deps thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
+  code_deps thy o snd o read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
 
 fun code_props_cmd raw_cs seris thy =
   let
     val (_, all_cs) = generate_const_exprs thy ["*"];
     val (permissive, cs) = generate_const_exprs thy raw_cs;