src/HOL/Tools/meson.ML

 
 
 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
 fun make_horns ths =
     name_thms "Horn#"
-      (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
+      (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.*)
 
 fun best_prolog_tac sizef horns =

 fun make_meta_clause th = 
     negated_asm_of_head (make_horn resolution_clause_rules (check_is_fol th));
 
 fun make_meta_clauses ths =
     name_thms "MClause#"
-      (gen_distinct Drule.eq_thm_prop (map make_meta_clause ths));
+      (distinct Drule.eq_thm_prop (map make_meta_clause ths));
 
 (*Permute a rule's premises to move the i-th premise to the last position.*)
 fun make_last i th =
   let val n = nprems_of th 
   in  if 1 <= i andalso i <= n