src/Pure/axclass.ML
changeset 44338 700008399ee5
parent 43329 84472e198515
child 50760 eee13361ec0a
     1.1 --- a/src/Pure/axclass.ML	Sat Aug 20 22:46:19 2011 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sat Aug 20 23:35:30 2011 +0200
     1.3 @@ -220,7 +220,9 @@
     1.4        in ((c1_pred, c2_succ), th') end;
     1.5  
     1.6      val new_classrels =
     1.7 -      Library.map_product pair (c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2)
     1.8 +      Library.map_product pair
     1.9 +        (c1 :: Graph.immediate_preds classes c1)
    1.10 +        (c2 :: Graph.immediate_succs classes c2)
    1.11        |> filter_out ((op =) orf Symreltab.defined classrels)
    1.12        |> map gen_classrel;
    1.13      val needed = not (null new_classrels);