# HG changeset patch
# User blanchet
# Date 1404994336 -7200
# Node ID 353fd33268353f8ecdecd68c709d2f7d92b9212d
# Parent  da5038b3886c5650cee6cb8f54d535cdeca155be
avoid loop in 'all_class_pairs' (caused by e.g. loading the 'Ceta' theory and calling Sledgehammer with the two facts 'fun_of_map.cases' and 'Lattices.bounded_lattice_top_class.sup_top_left' with a polymorphic type encoding)

diff -r da5038b3886c -r 353fd3326835 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 09 18:57:20 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jul 10 14:12:16 2014 +0200
@@ -472,15 +472,15 @@
 
 (* Proving one (tycon, class) membership may require proving others, so
    iterate. *)
-fun all_class_pairs _ _ [] = ([], [])
-  | all_class_pairs thy tycons cls =
+fun all_class_pairs _ _ _ [] = ([], [])
+  | all_class_pairs thy tycons old_cls cls =
     let
-      fun maybe_insert_class s =
-        (s <> class_of_types andalso not (member (op =) cls s)) ? insert (op =) s
+      val old_cls' = cls @ old_cls
+      fun maybe_insert_class s = not (member (op =) old_cls' s) ? insert (op =) s
+
       val pairs = class_pairs thy tycons cls
-      val new_cls =
-        [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) pairs
-      val (cls', pairs') = all_class_pairs thy tycons new_cls
+      val new_cls = fold (fold (fold (fold maybe_insert_class) o snd) o snd) pairs []
+      val (cls', pairs') = all_class_pairs thy tycons old_cls' new_cls
     in (cls' @ cls, union (op =) pairs' pairs) end
 
 fun tcon_clause _ _ [] = []
@@ -498,7 +498,7 @@
       tcon_clause (cl :: seen) n ((tcons, ars) :: rest)
 
 fun make_tcon_clauses thy tycons =
-  all_class_pairs thy tycons ##> tcon_clause [] 1
+  all_class_pairs thy tycons [] ##> tcon_clause [] 1
 
 
 (** Isabelle class relations **)