src/Pure/Isar/class_declaration.ML
changeset 58837 e84d900cd287
parent 58319 9228350683d0
child 58957 c9e744ea8a38
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Thu Oct 30 16:17:56 2014 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Thu Oct 30 16:20:46 2014 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4          val loc_intro_tac =
     1.5            (case Locale.intros_of thy class of
     1.6              (_, NONE) => all_tac
     1.7 -          | (_, SOME intro) => ALLGOALS (rtac intro));
     1.8 +          | (_, SOME intro) => ALLGOALS (resolve_tac [intro]));
     1.9          val tac = loc_intro_tac
    1.10            THEN ALLGOALS (Proof_Context.fact_tac empty_ctxt (sup_axioms @ the_list assm_axiom));
    1.11        in Element.prove_witness empty_ctxt prop tac end) some_prop;