src/HOL/Tools/ATP/res_clasimpset.ML
changeset 16957 8dcd14e8db7a
parent 16956 5b413c866593
child 17150 ce2a1aeb42aa
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Jul 28 17:56:27 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jul 29 15:20:29 2005 +0200
     1.3 @@ -110,6 +110,7 @@
     1.4  
     1.5    val relevant : int ref
     1.6    val use_simpset: bool ref
     1.7 +  val use_nameless: bool ref
     1.8    val write_out_clasimp : string -> theory -> term -> 
     1.9                               (ResClause.clause * thm) Array.array * int (* * ResClause.clause list *)
    1.10  
    1.11 @@ -118,16 +119,22 @@
    1.12  structure ResClasimp : RES_CLASIMP =
    1.13  struct
    1.14  val use_simpset = ref true;
    1.15 -(*Relevance filtering is off by default*)
    1.16 -val relevant = ref 0;  
    1.17 +val use_nameless = ref false;  (*Because most are useless [iff] rules*)
    1.18 +
    1.19 +val relevant = ref 0;  (*Relevance filtering is off by default*)
    1.20  
    1.21  (*The "name" of a theorem is its statement, if nothing else is available.*)
    1.22  val plain_string_of_thm =
    1.23      setmp show_question_marks false 
    1.24        (setmp print_mode [] 
    1.25  	(Pretty.setmp_margin 999 string_of_thm));
    1.26 +	
    1.27 +fun fake_thm_name th = 
    1.28 +    Context.theory_name (theory_of_thm th) ^ "." ^ 
    1.29 +    ResLib.trim_ends (plain_string_of_thm th);
    1.30  
    1.31 -fun put_name_pair ("",th) = (ResLib.trim_ends (plain_string_of_thm th), th)
    1.32 +fun put_name_pair ("",th) = if !use_nameless then (fake_thm_name th, th)
    1.33 +                            else ("HOL.TrueI",TrueI)
    1.34    | put_name_pair (a,th)  = (a,th);
    1.35  
    1.36  (* changed, now it also finds out the name of the theorem. *)