src/Pure/axclass.ML
changeset 59564 fdc03c8daacc
parent 59058 a78612c67ec0
child 59582 0fbed69ff081
     1.1 --- a/src/Pure/axclass.ML	Mon Feb 23 14:48:40 2015 +0100
     1.2 +++ b/src/Pure/axclass.ML	Mon Feb 23 14:50:30 2015 +0100
     1.3 @@ -457,7 +457,7 @@
     1.4      val names = map (prefix arity_prefix) (Logic.name_arities arity);
     1.5      val props = Logic.mk_arities arity;
     1.6      val ths =
     1.7 -      Goal.prove_multi ctxt [] [] props
     1.8 +      Goal.prove_common ctxt NONE [] [] props
     1.9        (fn {context, ...} => Goal.precise_conjunction_tac (length props) 1 THEN tac context)
    1.10          handle ERROR msg =>
    1.11            cat_error msg ("The error(s) above occurred while trying to prove type arity " ^