src/Pure/Isar/isar_cmd.ML
changeset 15964 f2074e12d1d4
parent 15799 50989ffdcdda
child 15979 c81578ac2d31
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon May 16 09:34:20 2005 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon May 16 09:35:05 2005 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4    val print_trans_rules: Toplevel.transition -> Toplevel.transition
     1.5    val print_methods: Toplevel.transition -> Toplevel.transition
     1.6    val print_antiquotations: Toplevel.transition -> Toplevel.transition
     1.7 -  val print_thms_containing: int option * string list
     1.8 +  val print_thms_containing: int option * (bool * ProofContext.search_criterion) list
     1.9      -> Toplevel.transition -> Toplevel.transition
    1.10    val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
    1.11    val print_binds: Toplevel.transition -> Toplevel.transition
    1.12 @@ -244,9 +244,22 @@
    1.13  
    1.14  val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
    1.15  
    1.16 -fun print_thms_containing (lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.17 -  ProofContext.print_thms_containing
    1.18 -    (Toplevel.node_case ProofContext.init Proof.context_of state) lim spec);
    1.19 +fun print_thms_containing (lim, spec) = Toplevel.unknown_theory o 
    1.20 +Toplevel.keep (fn state =>
    1.21 +  let
    1.22 +    fun get_goal () = 
    1.23 +      let val (_, (_, st)) = Proof.get_goal (Toplevel.proof_of state);
    1.24 +      in prop_of st end;
    1.25 +    
    1.26 +    (* searching is permitted without a goal.
    1.27 +       I am not sure whether the only exception that I should catch is UNDEF *)
    1.28 +    val goal = SOME (get_goal ()) handle Toplevel.UNDEF => NONE;
    1.29 +    
    1.30 +    val ctxt = (Toplevel.node_case ProofContext.init Proof.context_of state);
    1.31 +  in
    1.32 +    ProofContext.print_thms_containing ctxt goal lim spec
    1.33 +  end);
    1.34 +
    1.35  
    1.36  fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.37    ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state)));