--- a/src/Pure/proof_general.ML Mon Feb 03 11:06:06 2003 +0100
+++ b/src/Pure/proof_general.ML Mon Feb 03 11:07:09 2003 +0100
@@ -16,7 +16,6 @@
val options: (string * (string * (string * (unit -> string) * (string -> unit)))) list ref
val process_pgip: string -> unit
val thms_containing: string list -> unit
- val print_intros: unit -> unit
val help: unit -> unit
val show_context: unit -> theory
val kill_goal: unit -> unit
@@ -358,14 +357,6 @@
fun thms_containing ss =
ProofContext.print_thms_containing (ProofContext.init (the_context ())) None ss;
-fun print_intros() =
- let val proof_state = Toplevel.proof_of (Toplevel.get_state ())
- val (ctxt,(_,st)) = Proof.get_goal proof_state
- val prt_fact = ProofContext.pretty_fact ctxt
- val thy = ProofContext.theory_of ctxt
- val facts = map (apsnd single) (Goals.find_intros_goal thy st 1)
- in map prt_fact (rev facts) |> Pretty.chunks |> Pretty.writeln end
-
val welcome = priority o Session.welcome;
val help = welcome;
val show_context = Context.the_context;