src/Pure/Isar/class_declaration.ML
changeset 52732 b4da1f2ec73f
parent 52636 238cec044ebf
child 52788 da1fdbfebd39
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Thu Jul 25 16:46:53 2013 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Sat Jul 27 16:35:51 2013 +0200
     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 (Tactic.rtac intro));
     1.8 +          | (_, SOME intro) => ALLGOALS (rtac intro));
     1.9          val tac = loc_intro_tac
    1.10            THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom));
    1.11        in Element.prove_witness empty_ctxt prop tac end) some_prop;
    1.12 @@ -94,8 +94,8 @@
    1.13      val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
    1.14      val tac =
    1.15        REPEAT (SOMEGOAL
    1.16 -        (Tactic.match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
    1.17 -          ORELSE' Tactic.assume_tac));
    1.18 +        (match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
    1.19 +          ORELSE' assume_tac));
    1.20      val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (K tac);
    1.21  
    1.22    in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;