eliminated obsolete var morphism;
authorwenzelm
Wed Jan 21 22:26:49 2009 +0100 (2009-01-21)
changeset 29605f2924219125e
parent 29604 0e1723e91ef8
child 29606 fedb8be05f24
eliminated obsolete var morphism;
src/Pure/assumption.ML
src/Pure/morphism.ML
src/Pure/variable.ML
     1.1 --- a/src/Pure/assumption.ML	Wed Jan 21 22:26:49 2009 +0100
     1.2 +++ b/src/Pure/assumption.ML	Wed Jan 21 22:26:49 2009 +0100
     1.3 @@ -119,6 +119,6 @@
     1.4      val thm = export false inner outer;
     1.5      val term = export_term inner outer;
     1.6      val typ = Logic.type_map term;
     1.7 -  in Morphism.morphism {binding = I, var = I, typ = typ, term = term, fact = map thm} end;
     1.8 +  in Morphism.morphism {binding = I, typ = typ, term = term, fact = map thm} end;
     1.9  
    1.10  end;
     2.1 --- a/src/Pure/morphism.ML	Wed Jan 21 22:26:49 2009 +0100
     2.2 +++ b/src/Pure/morphism.ML	Wed Jan 21 22:26:49 2009 +0100
     2.3 @@ -16,7 +16,6 @@
     2.4  signature MORPHISM =
     2.5  sig
     2.6    include BASIC_MORPHISM
     2.7 -  val var: morphism -> binding * mixfix -> binding * mixfix
     2.8    val binding: morphism -> binding -> binding
     2.9    val typ: morphism -> typ -> typ
    2.10    val term: morphism -> term -> term
    2.11 @@ -25,12 +24,10 @@
    2.12    val cterm: morphism -> cterm -> cterm
    2.13    val morphism:
    2.14     {binding: binding -> binding,
    2.15 -    var: binding * mixfix -> binding * mixfix,
    2.16      typ: typ -> typ,
    2.17      term: term -> term,
    2.18      fact: thm list -> thm list} -> morphism
    2.19    val binding_morphism: (binding -> binding) -> morphism
    2.20 -  val var_morphism: (binding * mixfix -> binding * mixfix) -> morphism
    2.21    val typ_morphism: (typ -> typ) -> morphism
    2.22    val term_morphism: (term -> term) -> morphism
    2.23    val fact_morphism: (thm list -> thm list) -> morphism
    2.24 @@ -46,7 +43,6 @@
    2.25  
    2.26  datatype morphism = Morphism of
    2.27   {binding: binding -> binding,
    2.28 -  var: binding * mixfix -> binding * mixfix,
    2.29    typ: typ -> typ,
    2.30    term: term -> term,
    2.31    fact: thm list -> thm list};
    2.32 @@ -54,7 +50,6 @@
    2.33  type declaration = morphism -> Context.generic -> Context.generic;
    2.34  
    2.35  fun binding (Morphism {binding, ...}) = binding;
    2.36 -fun var (Morphism {var, ...}) = var;
    2.37  fun typ (Morphism {typ, ...}) = typ;
    2.38  fun term (Morphism {term, ...}) = term;
    2.39  fun fact (Morphism {fact, ...}) = fact;
    2.40 @@ -63,20 +58,19 @@
    2.41  
    2.42  val morphism = Morphism;
    2.43  
    2.44 -fun binding_morphism binding = morphism {binding = binding, var = I, typ = I, term = I, fact = I};
    2.45 -fun var_morphism var = morphism {binding = I, var = var, typ = I, term = I, fact = I};
    2.46 -fun typ_morphism typ = morphism {binding = I, var = I, typ = typ, term = I, fact = I};
    2.47 -fun term_morphism term = morphism {binding = I, var = I, typ = I, term = term, fact = I};
    2.48 -fun fact_morphism fact = morphism {binding = I, var = I, typ = I, term = I, fact = fact};
    2.49 -fun thm_morphism thm = morphism {binding = I, var = I, typ = I, term = I, fact = map thm};
    2.50 +fun binding_morphism binding = morphism {binding = binding, typ = I, term = I, fact = I};
    2.51 +fun typ_morphism typ = morphism {binding = I, typ = typ, term = I, fact = I};
    2.52 +fun term_morphism term = morphism {binding = I, typ = I, term = term, fact = I};
    2.53 +fun fact_morphism fact = morphism {binding = I, typ = I, term = I, fact = fact};
    2.54 +fun thm_morphism thm = morphism {binding = I, typ = I, term = I, fact = map thm};
    2.55  
    2.56 -val identity = morphism {binding = I, var = I, typ = I, term = I, fact = I};
    2.57 +val identity = morphism {binding = I, typ = I, term = I, fact = I};
    2.58  
    2.59  fun compose
    2.60 -    (Morphism {binding = binding1, var = var1, typ = typ1, term = term1, fact = fact1})
    2.61 -    (Morphism {binding = binding2, var = var2, typ = typ2, term = term2, fact = fact2}) =
    2.62 -  morphism {binding = binding1 o binding2, var = var1 o var2,
    2.63 -    typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2};
    2.64 +    (Morphism {binding = binding1, typ = typ1, term = term1, fact = fact1})
    2.65 +    (Morphism {binding = binding2, typ = typ2, term = term2, fact = fact2}) =
    2.66 +  morphism {binding = binding1 o binding2, typ = typ1 o typ2,
    2.67 +    term = term1 o term2, fact = fact1 o fact2};
    2.68  
    2.69  fun phi1 $> phi2 = compose phi2 phi1;
    2.70  
     3.1 --- a/src/Pure/variable.ML	Wed Jan 21 22:26:49 2009 +0100
     3.2 +++ b/src/Pure/variable.ML	Wed Jan 21 22:26:49 2009 +0100
     3.3 @@ -397,7 +397,7 @@
     3.4      val fact = export inner outer;
     3.5      val term = singleton (export_terms inner outer);
     3.6      val typ = Logic.type_map term;
     3.7 -  in Morphism.morphism {binding = I, var = I, typ = typ, term = term, fact = fact} end;
     3.8 +  in Morphism.morphism {binding = I, typ = typ, term = term, fact = fact} end;
     3.9  
    3.10  
    3.11