diff -r df7aac8543c9 -r 3d1e7a199bdc src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/HOL/Tools/meson.ML	Tue May 07 14:26:32 2002 +0200
@@ -266,7 +266,7 @@
 (*Convert a list of clauses to (contrapositive) Horn clauses*)
 fun make_horns ths =
     name_thms "Horn#"
-      (gen_distinct eq_thm (foldr (add_contras clause_rules) (ths,[])));
+      (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) (ths,[])));
 
 (*Could simply use nprems_of, which would count remaining subgoals -- no
   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)