changeset 58837 | e84d900cd287 |
parent 58668 | 1891f17c6124 |
child 59058 | a78612c67ec0 |
--- a/src/Pure/Isar/class.ML Thu Oct 30 16:17:56 2014 +0100 +++ b/src/Pure/Isar/class.ML Thu Oct 30 16:20:46 2014 +0100 @@ -434,7 +434,7 @@ (fst o rules thy) sub]; val classrel = Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup)) - (K (EVERY (map (TRYALL o rtac) intros))); + (K (EVERY (map (TRYALL o resolve_tac o single) intros))); val diff_sort = Sign.complete_sort thy [sup] |> subtract (op =) (Sign.complete_sort thy [sub]) |> filter (is_class thy);