src/Pure/Isar/class_declaration.ML
changeset 52636 238cec044ebf
parent 51685 385ef6706252
child 52732 b4da1f2ec73f
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Sat Jul 13 13:03:21 2013 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Sat Jul 13 17:53:57 2013 +0200
     1.3 @@ -49,8 +49,8 @@
     1.4          locale.ML / expression.ML would be desirable*)
     1.5  
     1.6      (* witness for canonical interpretation *)
     1.7 -    val prop = try the_single props;
     1.8 -    val wit = Option.map (fn prop =>
     1.9 +    val some_prop = try the_single props;
    1.10 +    val some_witn = Option.map (fn prop =>
    1.11        let
    1.12          val sup_axioms = map_filter (fst o Class.rules thy) sups;
    1.13          val loc_intro_tac =
    1.14 @@ -59,13 +59,13 @@
    1.15            | (_, SOME intro) => ALLGOALS (Tactic.rtac intro));
    1.16          val tac = loc_intro_tac
    1.17            THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom));
    1.18 -      in Element.prove_witness empty_ctxt prop tac end) prop;
    1.19 -    val axiom = Option.map Element.conclude_witness wit;
    1.20 +      in Element.prove_witness empty_ctxt prop tac end) some_prop;
    1.21 +    val some_axiom = Option.map Element.conclude_witness some_witn;
    1.22  
    1.23      (* canonical interpretation *)
    1.24      val base_morph = inst_morph
    1.25        $> Morphism.binding_morphism (Binding.prefix false (Class.class_prefix class))
    1.26 -      $> Element.satisfy_morphism (the_list wit);
    1.27 +      $> Element.satisfy_morphism (the_list some_witn);
    1.28      val eq_morph = Element.eq_morphism thy (Class.these_defs thy sups);
    1.29  
    1.30      (* assm_intro *)
    1.31 @@ -79,12 +79,12 @@
    1.32          val thm'' = Morphism.thm const_eq_morph thm';
    1.33          val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
    1.34        in Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'') (K tac) end;
    1.35 -    val assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
    1.36 +    val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
    1.37  
    1.38      (* of_class *)
    1.39      val of_class_prop_concl = Logic.mk_of_class (aT, class);
    1.40      val of_class_prop =
    1.41 -      (case prop of
    1.42 +      (case some_prop of
    1.43          NONE => of_class_prop_concl
    1.44        | SOME prop => Logic.mk_implies (Morphism.term const_morph
    1.45            ((map_types o map_atyps) (K aT) prop), of_class_prop_concl));
    1.46 @@ -98,7 +98,7 @@
    1.47            ORELSE' Tactic.assume_tac));
    1.48      val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (K tac);
    1.49  
    1.50 -  in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end;
    1.51 +  in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;
    1.52  
    1.53  
    1.54  (* reading and processing class specifications *)
    1.55 @@ -317,10 +317,10 @@
    1.56      ||> Theory.checkpoint
    1.57      |-> (fn (param_map, params, assm_axiom) =>
    1.58         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
    1.59 -    #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
    1.60 +    #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
    1.61         Context.theory_map (Locale.add_registration (class, base_morph)
    1.62           (Option.map (rpair true) eq_morph) export_morph)
    1.63 -    #> Class.register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
    1.64 +    #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class))
    1.65      |> Named_Target.init before_exit class
    1.66      |> pair class
    1.67    end;