Tactic.precise_conjunction_tac;
authorwenzelm
Thu Dec 22 00:28:53 2005 +0100 (2005-12-22 ago)
changeset 18467bb7b309ac395
parent 18466 389a6f9c31f4
child 18468 43951ffb6304
Tactic.precise_conjunction_tac;
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Thu Dec 22 00:28:52 2005 +0100
     1.2 +++ b/src/Pure/axclass.ML	Thu Dec 22 00:28:53 2005 +0100
     1.3 @@ -283,8 +283,9 @@
     1.4      val _ = message ("Proving type arity " ^ txt ^ " ...");
     1.5      val props = (mk_arities arity);
     1.6      val ths = Goal.prove_multi thy [] [] props
     1.7 -      (fn _ => Tactic.smart_conjunction_tac (length props) THEN tac) handle ERROR_MESSAGE msg =>
     1.8 -        error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
     1.9 +      (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac)
    1.10 +        handle ERROR_MESSAGE msg =>
    1.11 +          error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
    1.12    in add_arity_thms ths thy end;
    1.13  
    1.14  in