src/HOL/Tools/ATP/recon_order_clauses.ML
changeset 15739 bb2acfed8212
parent 15702 2677db44c795
child 15774 9df37a0e935d
     1.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Fri Apr 15 17:03:35 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Fri Apr 15 18:16:05 2005 +0200
     1.3 @@ -228,28 +228,27 @@
     1.4  
     1.5  fun is_alpha_space_or_neg_or_eq ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=")
     1.6  
     1.7 -fun lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t
     1.8 +fun lit_string sg t = 
     1.9 +                   let val termstr = Sign.string_of_term sg t
    1.10                         val exp_term = explode termstr
    1.11                     in
    1.12                         implode(List.filter is_alpha_space_or_neg_or_eq exp_term)
    1.13                     end
    1.14  
    1.15 -fun get_meta_lits thm = map lit_string (prems_of thm)
    1.16 -
    1.17 +fun get_meta_lits thm = map (lit_string (sign_of_thm thm)) (prems_of thm)
    1.18  
    1.19  
    1.20 +fun is_alpha_space_or_neg_or_eq_or_bracket ch = is_alpha_space_or_neg_or_eq ch orelse (ch= "(") orelse (ch = ")")
    1.21  
    1.22 -fun is_alpha_space_or_neg_or_eq_or_bracket ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=") orelse (ch= "(") orelse (ch = ")")
    1.23 -
    1.24 -fun lit_string_bracket  t = let val termstr = (Sign.string_of_term Mainsign ) t
    1.25 +fun lit_string_bracket sg t = 
    1.26 +                   let val termstr = Sign.string_of_term sg t
    1.27                         val exp_term = explode termstr
    1.28                     in
    1.29                         implode(List.filter  is_alpha_space_or_neg_or_eq_or_bracket exp_term)
    1.30                     end
    1.31  
    1.32 -fun get_meta_lits_bracket thm = map lit_string_bracket (prems_of thm)
    1.33 -
    1.34 -
    1.35 +fun get_meta_lits_bracket thm = 
    1.36 +    map (lit_string_bracket (sign_of_thm thm)) (prems_of thm)
    1.37  
    1.38        
    1.39  fun apply_rule rule [] thm = thm