1.1 --- a/src/HOL/Tools/meson.ML	Mon Feb 26 21:34:16 2007 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Mon Feb 26 23:18:24 2007 +0100
     1.3 @@ -498,7 +498,7 @@
     1.4  (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
     1.5  fun make_horns ths =
     1.6      name_thms "Horn#"
     1.7 -      (distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
     1.8 +      (distinct Thm.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
     1.9  
    1.10  (*Could simply use nprems_of, which would count remaining subgoals -- no
    1.11    discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
    1.12 @@ -609,7 +609,7 @@
    1.13    
    1.14  fun make_meta_clauses ths =
    1.15      name_thms "MClause#"
    1.16 -      (distinct Drule.eq_thm_prop (map make_meta_clause ths));
    1.17 +      (distinct Thm.eq_thm_prop (map make_meta_clause ths));
    1.18  
    1.19  (*Permute a rule's premises to move the i-th premise to the last position.*)
    1.20  fun make_last i th =