src/Pure/Isar/isar_cmd.ML

   val immediate_proof: Toplevel.transition -> Toplevel.transition
   val done_proof: Toplevel.transition -> Toplevel.transition
   val skip_proof: Toplevel.transition -> Toplevel.transition
   val init_theory: string * string list * (string * bool) list ->
     Toplevel.transition -> Toplevel.transition
-  val welcome: Toplevel.transition -> Toplevel.transition
   val exit: Toplevel.transition -> Toplevel.transition
   val quit: Toplevel.transition -> Toplevel.transition
   val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
   val disable_pr: Toplevel.transition -> Toplevel.transition
   val enable_pr: Toplevel.transition -> Toplevel.transition

   val print_methods: Toplevel.transition -> Toplevel.transition
   val print_antiquotations: Toplevel.transition -> Toplevel.transition
   val class_deps: Toplevel.transition -> Toplevel.transition
   val thy_deps: Toplevel.transition -> Toplevel.transition
   val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
-  val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list
-    -> Toplevel.transition -> Toplevel.transition
-  val find_consts: (bool * FindConsts.criterion) list ->
-                   Toplevel.transition -> Toplevel.transition
   val unused_thms: (string list * string list option) option ->
     Toplevel.transition -> Toplevel.transition
   val print_binds: Toplevel.transition -> Toplevel.transition
   val print_cases: Toplevel.transition -> Toplevel.transition
   val print_stmts: string list * (Facts.ref * Attrib.src list) list

 
 
 (* axioms *)
 
 fun add_axms f args thy =
-  f (map (fn ((b, ax), srcs) => ((Binding.base_name b, ax), map (Attrib.attribute thy) srcs)) args) thy;
+  f (map (fn ((b, ax), srcs) => ((Binding.name_of b, ax), map (Attrib.attribute thy) srcs)) args) thy;
 
 val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
 
 fun add_defs ((unchecked, overloaded), args) =
   add_axms

   Toplevel.init_theory name (ThyInfo.begin_theory name imports (map (apfst Path.explode) uses))
     (fn thy =>
       if ThyInfo.check_known_thy (Context.theory_name thy)
       then ThyInfo.end_theory thy else ());
 
-val welcome = Toplevel.imperative (writeln o Session.welcome);
-
 val exit = Toplevel.keep (fn state =>
  (Context.set_thread_data (try Toplevel.generic_theory_of state);
   raise Toplevel.TERMINATE));
 
 val quit = Toplevel.imperative quit;

     val gr =
       Graph.fold (cons o entry) classes []
       |> sort (int_ord o pairself #1) |> map #2;
   in Present.display_graph gr end);
 
-
-(* retrieve theorems *)
-
 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
-
-fun find_theorems ((opt_lim, rem_dups), spec) =
-  Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  let
-    val proof_state = Toplevel.enter_proof_body state;
-    val ctxt = Proof.context_of proof_state;
-    val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2);
-  in FindTheorems.print_theorems ctxt opt_goal opt_lim rem_dups spec end);
 
 
 (* find unused theorems *)
 
 fun unused_thms opt_range = Toplevel.keep (fn state =>

       | SOME (xs, NONE) => (map ThyInfo.get_theory xs, [thy])
       | SOME (xs, SOME ys) => (map ThyInfo.get_theory xs, map ThyInfo.get_theory ys))
     |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
   end);
 
-(* retrieve constants *)
-
-fun find_consts spec =
-  Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  let val ctxt = (Proof.context_of o Toplevel.enter_proof_body) state
-  in FindConsts.find_consts ctxt spec end);
 
 (* print proof context contents *)
 
 val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state =>
   ProofContext.setmp_verbose ProofContext.print_binds (Toplevel.context_of state));