src/Pure/Isar/class_declaration.ML
changeset 54742 7a86358a3c0b
parent 54740 91f54d386680
child 54866 7b9a67cbd48f
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4              (_, NONE) => all_tac
     1.5            | (_, SOME intro) => ALLGOALS (rtac intro));
     1.6          val tac = loc_intro_tac
     1.7 -          THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom));
     1.8 +          THEN ALLGOALS (Proof_Context.fact_tac empty_ctxt (sup_axioms @ the_list assm_axiom));
     1.9        in Element.prove_witness empty_ctxt prop tac end) some_prop;
    1.10      val some_axiom = Option.map Element.conclude_witness some_witn;
    1.11  
    1.12 @@ -77,8 +77,10 @@
    1.13              SOME eq_morph => const_morph $> eq_morph
    1.14            | NONE => const_morph);
    1.15          val thm'' = Morphism.thm const_eq_morph thm';
    1.16 -        val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
    1.17 -      in Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'') (K tac) end;
    1.18 +      in
    1.19 +        Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'')
    1.20 +          (fn {context = ctxt, ...} => ALLGOALS (Proof_Context.fact_tac ctxt [thm'']))
    1.21 +      end;
    1.22      val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
    1.23  
    1.24      (* of_class *)