1.1 --- a/src/HOL/Tools/functorial_mappers.ML	Thu Nov 18 17:01:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/functorial_mappers.ML	Thu Nov 18 17:06:02 2010 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  structure Functorial_Mappers : FUNCTORIAL_MAPPERS =
     1.5  struct
     1.6  
     1.7 -val concatenateN = "concatenate";
     1.8 +val compositionalityN = "compositionality";
     1.9  val identityN = "identity";
    1.10  
    1.11  (** functorial mappers and their properties **)
    1.12 @@ -25,7 +25,7 @@
    1.13  (* bookkeeping *)
    1.14  
    1.15  type entry = { mapper: string, variances: (sort * (bool * bool)) list,
    1.16 -  concatenate: thm, identity: thm };
    1.17 +  compositionality: thm, identity: thm };
    1.18  
    1.19  structure Data = Theory_Data(
    1.20    type T = entry Symtab.table
    1.21 @@ -74,7 +74,7 @@
    1.22  
    1.23  (* mapper properties *)
    1.24  
    1.25 -fun make_concatenate_prop variances (tyco, mapper) =
    1.26 +fun make_compositionality_prop variances (tyco, mapper) =
    1.27    let
    1.28      fun invents n k nctxt =
    1.29        let
    1.30 @@ -186,23 +186,23 @@
    1.31         of [tyco] => tyco
    1.32          | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
    1.33      val variances = analyze_variances thy tyco T;
    1.34 -    val concatenate_prop = uncurry (fold_rev Logic.all)
    1.35 -      (make_concatenate_prop variances (tyco, mapper));
    1.36 +    val compositionality_prop = uncurry (fold_rev Logic.all)
    1.37 +      (make_compositionality_prop variances (tyco, mapper));
    1.38      val identity_prop = uncurry Logic.all
    1.39        (make_identity_prop variances (tyco, mapper));
    1.40      val qualify = Binding.qualify true (Long_Name.base_name mapper) o Binding.name;
    1.41 -    fun after_qed [single_concatenate, single_identity] lthy =
    1.42 +    fun after_qed [single_compositionality, single_identity] lthy =
    1.43        lthy
    1.44 -      |> Local_Theory.note ((qualify concatenateN, []), single_concatenate)
    1.45 +      |> Local_Theory.note ((qualify compositionalityN, []), single_compositionality)
    1.46        ||>> Local_Theory.note ((qualify identityN, []), single_identity)
    1.47 -      |-> (fn ((_, [concatenate]), (_, [identity])) =>
    1.48 +      |-> (fn ((_, [compositionality]), (_, [identity])) =>
    1.49            (Local_Theory.background_theory o Data.map)
    1.50              (Symtab.update (tyco, { mapper = mapper, variances = variances,
    1.51 -              concatenate = concatenate, identity = identity })));
    1.52 +              compositionality = compositionality, identity = identity })));
    1.53    in
    1.54      thy
    1.55      |> Named_Target.theory_init
    1.56 -    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [concatenate_prop, identity_prop])
    1.57 +    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [compositionality_prop, identity_prop])
    1.58    end
    1.59  
    1.60  val type_mapper = gen_type_mapper Sign.cert_term;