FindTheorems.print_theorems;
authorwenzelm
Sun May 22 16:51:10 2005 +0200 (2005-05-22)
changeset 1602296a9bf7ac18d
parent 16021 ff83bc2151bf
child 16023 66561f6814bd
FindTheorems.print_theorems;
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Sun May 22 16:51:09 2005 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Sun May 22 16:51:10 2005 +0200
     1.3 @@ -371,13 +371,12 @@
     1.4  
     1.5  end
     1.6  
     1.7 +
     1.8  (* misc commands for ProofGeneral/isa *)
     1.9  
    1.10 -(* PG/isa mode does not go through the Isar parser, hence we 
    1.11 -   interpret everything as term pattern only *)
    1.12  fun thms_containing ss =
    1.13 -  ProofContext.print_thms_containing (ProofContext.init (the_context ())) NONE NONE 
    1.14 -    (map (fn s => (true, ProofContext.Pattern s)) ss);
    1.15 +  FindTheorems.print_theorems (ProofContext.init (the_context ())) NONE NONE 
    1.16 +    (map (fn s => (true, FindTheorems.Pattern s)) ss);
    1.17  
    1.18  val welcome = priority o Session.welcome;
    1.19  val help = welcome;