src/HOL/Tools/meson.ML
changeset 13105 3d1e7a199bdc
parent 12299 2c76042c3b06
child 14733 3eda95792083
     1.1 --- a/src/HOL/Tools/meson.ML	Tue May 07 14:24:30 2002 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Tue May 07 14:26:32 2002 +0200
     1.3 @@ -266,7 +266,7 @@
     1.4  (*Convert a list of clauses to (contrapositive) Horn clauses*)
     1.5  fun make_horns ths =
     1.6      name_thms "Horn#"
     1.7 -      (gen_distinct eq_thm (foldr (add_contras clause_rules) (ths,[])));
     1.8 +      (gen_distinct Drule.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.*)