tuned variable names
authorhaftmann
Sat Jul 13 17:53:57 2013 +0200 (2013-07-13)
changeset 52636238cec044ebf
parent 52635 4f84b730c489
child 52637 1501ebe39711
tuned variable names
src/Pure/Isar/class.ML
src/Pure/Isar/class_declaration.ML
     1.1 --- a/src/Pure/Isar/class.ML	Sat Jul 13 13:03:21 2013 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sat Jul 13 17:53:57 2013 +0200
     1.3 @@ -211,13 +211,13 @@
     1.4  (* updaters *)
     1.5  
     1.6  fun register class sups params base_sort base_morph export_morph
     1.7 -    axiom assm_intro of_class thy =
     1.8 +    some_axiom some_assm_intro of_class thy =
     1.9    let
    1.10      val operations = map (fn (v_ty as (_, ty), (c, _)) =>
    1.11        (c, (class, (ty, Free v_ty)))) params;
    1.12      val add_class = Graph.new_node (class,
    1.13          make_class_data (((map o pairself) fst params, base_sort,
    1.14 -          base_morph, export_morph, assm_intro, of_class, axiom), ([], operations)))
    1.15 +          base_morph, export_morph, some_assm_intro, of_class, some_axiom), ([], operations)))
    1.16        #> fold (curry Graph.add_edge class) sups;
    1.17    in Class_Data.map add_class thy end;
    1.18  
    1.19 @@ -245,10 +245,10 @@
    1.20      |> activate_defs class (the_list some_def)
    1.21    end;
    1.22  
    1.23 -fun register_subclass (sub, sup) some_dep_morph some_wit export thy =
    1.24 +fun register_subclass (sub, sup) some_dep_morph some_witn export thy =
    1.25    let
    1.26      val intros = (snd o rules thy) sup :: map_filter I
    1.27 -      [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit,
    1.28 +      [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_witn,
    1.29          (fst o rules thy) sub];
    1.30      val classrel =
    1.31        Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup))
    1.32 @@ -259,7 +259,7 @@
    1.33      val add_dependency =
    1.34        (case some_dep_morph of
    1.35          SOME dep_morph => Locale.add_dependency sub
    1.36 -          (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) NONE export
    1.37 +          (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)) NONE export
    1.38        | NONE => I);
    1.39    in
    1.40      thy
     2.1 --- a/src/Pure/Isar/class_declaration.ML	Sat Jul 13 13:03:21 2013 +0200
     2.2 +++ b/src/Pure/Isar/class_declaration.ML	Sat Jul 13 17:53:57 2013 +0200
     2.3 @@ -49,8 +49,8 @@
     2.4          locale.ML / expression.ML would be desirable*)
     2.5  
     2.6      (* witness for canonical interpretation *)
     2.7 -    val prop = try the_single props;
     2.8 -    val wit = Option.map (fn prop =>
     2.9 +    val some_prop = try the_single props;
    2.10 +    val some_witn = Option.map (fn prop =>
    2.11        let
    2.12          val sup_axioms = map_filter (fst o Class.rules thy) sups;
    2.13          val loc_intro_tac =
    2.14 @@ -59,13 +59,13 @@
    2.15            | (_, SOME intro) => ALLGOALS (Tactic.rtac intro));
    2.16          val tac = loc_intro_tac
    2.17            THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom));
    2.18 -      in Element.prove_witness empty_ctxt prop tac end) prop;
    2.19 -    val axiom = Option.map Element.conclude_witness wit;
    2.20 +      in Element.prove_witness empty_ctxt prop tac end) some_prop;
    2.21 +    val some_axiom = Option.map Element.conclude_witness some_witn;
    2.22  
    2.23      (* canonical interpretation *)
    2.24      val base_morph = inst_morph
    2.25        $> Morphism.binding_morphism (Binding.prefix false (Class.class_prefix class))
    2.26 -      $> Element.satisfy_morphism (the_list wit);
    2.27 +      $> Element.satisfy_morphism (the_list some_witn);
    2.28      val eq_morph = Element.eq_morphism thy (Class.these_defs thy sups);
    2.29  
    2.30      (* assm_intro *)
    2.31 @@ -79,12 +79,12 @@
    2.32          val thm'' = Morphism.thm const_eq_morph thm';
    2.33          val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
    2.34        in Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'') (K tac) end;
    2.35 -    val assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
    2.36 +    val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
    2.37  
    2.38      (* of_class *)
    2.39      val of_class_prop_concl = Logic.mk_of_class (aT, class);
    2.40      val of_class_prop =
    2.41 -      (case prop of
    2.42 +      (case some_prop of
    2.43          NONE => of_class_prop_concl
    2.44        | SOME prop => Logic.mk_implies (Morphism.term const_morph
    2.45            ((map_types o map_atyps) (K aT) prop), of_class_prop_concl));
    2.46 @@ -98,7 +98,7 @@
    2.47            ORELSE' Tactic.assume_tac));
    2.48      val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (K tac);
    2.49  
    2.50 -  in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end;
    2.51 +  in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;
    2.52  
    2.53  
    2.54  (* reading and processing class specifications *)
    2.55 @@ -317,10 +317,10 @@
    2.56      ||> Theory.checkpoint
    2.57      |-> (fn (param_map, params, assm_axiom) =>
    2.58         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
    2.59 -    #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
    2.60 +    #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
    2.61         Context.theory_map (Locale.add_registration (class, base_morph)
    2.62           (Option.map (rpair true) eq_morph) export_morph)
    2.63 -    #> Class.register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
    2.64 +    #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class))
    2.65      |> Named_Target.init before_exit class
    2.66      |> pair class
    2.67    end;