# HG changeset patch
# User berghofe
# Date 1044266829 -3600
# Node ID 6c5c5bdfae84ead5774515a2dcb65cab1dbd13e2
# Parent  16136d2da0db9273792d2164b4c9da95e459286d
Moved print_intros from proof_general.ML to Isar/isar_cmd.ML

diff -r 16136d2da0db -r 6c5c5bdfae84 src/Pure/Isar/isar_cmd.ML
--- 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 *)
 
diff -r 16136d2da0db -r 6c5c5bdfae84 src/Pure/proof_general.ML
--- 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;