src/Pure/Isar/class_declaration.ML
changeset 70309 f9fd15d3cfac
parent 69058 f4fb93197670
child 70387 35dd9212bf29
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Mon Jun 03 15:40:08 2019 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Mon Jun 03 17:01:28 2019 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  
     1.5  fun calculate thy class sups base_sort param_map assm_axiom =
     1.6    let
     1.7 -    val empty_ctxt = Proof_Context.init_global thy;
     1.8 +    val thy_ctxt = Proof_Context.init_global thy;
     1.9  
    1.10      val certT = Thm.trim_context_ctyp o Thm.global_ctyp_of thy;
    1.11      val cert = Thm.trim_context_cterm o Thm.global_cterm_of thy;
    1.12 @@ -42,7 +42,7 @@
    1.13        Element.instantiate_normalize_morphism ([], param_map_inst);
    1.14      val typ_morph =
    1.15        Element.instantiate_normalize_morphism ([(a_tfree, certT (TFree (Name.aT, [class])))], [])
    1.16 -    val (([raw_props], _, [(_, raw_inst_morph)], _, export_morph), _) = empty_ctxt
    1.17 +    val (([raw_props], _, [(_, raw_inst_morph)], _, export_morph), _) = thy_ctxt
    1.18        |> Expression.cert_goal_expression ([(class, (("", false),
    1.19             (Expression.Named param_map_const, [])))], []);
    1.20      val (props, inst_morph) =
    1.21 @@ -60,11 +60,11 @@
    1.22          val loc_intro_tac =
    1.23            (case Locale.intros_of thy class of
    1.24              (_, NONE) => all_tac
    1.25 -          | (_, SOME intro) => ALLGOALS (resolve_tac empty_ctxt [intro]));
    1.26 +          | (_, SOME intro) => ALLGOALS (resolve_tac thy_ctxt [intro]));
    1.27          val tac = loc_intro_tac
    1.28 -          THEN ALLGOALS (Proof_Context.fact_tac empty_ctxt (sup_axioms @ the_list assm_axiom));
    1.29 -      in Element.prove_witness empty_ctxt prop tac end) some_prop;
    1.30 -    val some_axiom = Option.map (Element.conclude_witness empty_ctxt) some_witn;
    1.31 +          THEN ALLGOALS (Proof_Context.fact_tac thy_ctxt (sup_axioms @ the_list assm_axiom));
    1.32 +      in Element.prove_witness thy_ctxt prop tac end) some_prop;
    1.33 +    val some_axiom = Option.map (Element.conclude_witness thy_ctxt) some_witn;
    1.34  
    1.35      (* canonical interpretation *)
    1.36      val base_morph = inst_morph
    1.37 @@ -75,7 +75,7 @@
    1.38      (* assm_intro *)
    1.39      fun prove_assm_intro thm =
    1.40        let
    1.41 -        val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
    1.42 +        val ((_, [thm']), _) = Variable.import true [thm] thy_ctxt;
    1.43          val const_eq_morph =
    1.44            (case eq_morph of
    1.45              SOME eq_morph => const_morph $> eq_morph