--- a/src/Pure/Isar/isar_cmd.ML Mon Feb 03 11:06:06 2003 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Mon Feb 03 11:07:09 2003 +0100
@@ -60,6 +60,7 @@
val print_binds: Toplevel.transition -> Toplevel.transition
val print_lthms: Toplevel.transition -> Toplevel.transition
val print_cases: Toplevel.transition -> Toplevel.transition
+ val print_intros: Toplevel.transition -> Toplevel.transition
val print_thms: string list * (string * Args.src list) list
-> Toplevel.transition -> Toplevel.transition
val print_prfs: bool -> string list * (string * Args.src list) list option
@@ -247,6 +248,14 @@
ProofContext.setmp_verbose
ProofContext.print_cases (Proof.context_of (Toplevel.proof_of state)));
+val print_intros = Toplevel.unknown_proof o Toplevel.keep (fn state =>
+ let
+ val (ctxt, (_, st)) = Proof.get_goal (Toplevel.proof_of state)
+ val prt_fact = ProofContext.pretty_fact ctxt
+ val thy = ProofContext.theory_of ctxt
+ val facts = map (apsnd single) (PureThy.find_intros_goal thy st 1)
+ in map prt_fact (rev facts) |> Pretty.chunks |> Pretty.writeln end);
+
(* print theorems / types / terms / props *)
--- 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;