src/Pure/Isar/class_declaration.ML
changeset 58957 c9e744ea8a38
parent 58837 e84d900cd287
child 58963 26bf09b95dda
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -94,11 +94,11 @@
     1.4      val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
     1.5      val axclass_intro = #intro (Axclass.get_info thy class);
     1.6      val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
     1.7 -    val tac =
     1.8 +    fun tac ctxt =
     1.9        REPEAT (SOMEGOAL
    1.10 -        (match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
    1.11 +        (match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
    1.12            ORELSE' assume_tac));
    1.13 -    val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (K tac);
    1.14 +    val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context);
    1.15  
    1.16    in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;
    1.17