src/Pure/morphism.ML
changeset 29605 f2924219125e
parent 29581 b3b33e0298eb
child 37216 3165bc303f66
     1.1 --- a/src/Pure/morphism.ML	Wed Jan 21 22:26:49 2009 +0100
     1.2 +++ b/src/Pure/morphism.ML	Wed Jan 21 22:26:49 2009 +0100
     1.3 @@ -16,7 +16,6 @@
     1.4  signature MORPHISM =
     1.5  sig
     1.6    include BASIC_MORPHISM
     1.7 -  val var: morphism -> binding * mixfix -> binding * mixfix
     1.8    val binding: morphism -> binding -> binding
     1.9    val typ: morphism -> typ -> typ
    1.10    val term: morphism -> term -> term
    1.11 @@ -25,12 +24,10 @@
    1.12    val cterm: morphism -> cterm -> cterm
    1.13    val morphism:
    1.14     {binding: binding -> binding,
    1.15 -    var: binding * mixfix -> binding * mixfix,
    1.16      typ: typ -> typ,
    1.17      term: term -> term,
    1.18      fact: thm list -> thm list} -> morphism
    1.19    val binding_morphism: (binding -> binding) -> morphism
    1.20 -  val var_morphism: (binding * mixfix -> binding * mixfix) -> morphism
    1.21    val typ_morphism: (typ -> typ) -> morphism
    1.22    val term_morphism: (term -> term) -> morphism
    1.23    val fact_morphism: (thm list -> thm list) -> morphism
    1.24 @@ -46,7 +43,6 @@
    1.25  
    1.26  datatype morphism = Morphism of
    1.27   {binding: binding -> binding,
    1.28 -  var: binding * mixfix -> binding * mixfix,
    1.29    typ: typ -> typ,
    1.30    term: term -> term,
    1.31    fact: thm list -> thm list};
    1.32 @@ -54,7 +50,6 @@
    1.33  type declaration = morphism -> Context.generic -> Context.generic;
    1.34  
    1.35  fun binding (Morphism {binding, ...}) = binding;
    1.36 -fun var (Morphism {var, ...}) = var;
    1.37  fun typ (Morphism {typ, ...}) = typ;
    1.38  fun term (Morphism {term, ...}) = term;
    1.39  fun fact (Morphism {fact, ...}) = fact;
    1.40 @@ -63,20 +58,19 @@
    1.41  
    1.42  val morphism = Morphism;
    1.43  
    1.44 -fun binding_morphism binding = morphism {binding = binding, var = I, typ = I, term = I, fact = I};
    1.45 -fun var_morphism var = morphism {binding = I, var = var, typ = I, term = I, fact = I};
    1.46 -fun typ_morphism typ = morphism {binding = I, var = I, typ = typ, term = I, fact = I};
    1.47 -fun term_morphism term = morphism {binding = I, var = I, typ = I, term = term, fact = I};
    1.48 -fun fact_morphism fact = morphism {binding = I, var = I, typ = I, term = I, fact = fact};
    1.49 -fun thm_morphism thm = morphism {binding = I, var = I, typ = I, term = I, fact = map thm};
    1.50 +fun binding_morphism binding = morphism {binding = binding, typ = I, term = I, fact = I};
    1.51 +fun typ_morphism typ = morphism {binding = I, typ = typ, term = I, fact = I};
    1.52 +fun term_morphism term = morphism {binding = I, typ = I, term = term, fact = I};
    1.53 +fun fact_morphism fact = morphism {binding = I, typ = I, term = I, fact = fact};
    1.54 +fun thm_morphism thm = morphism {binding = I, typ = I, term = I, fact = map thm};
    1.55  
    1.56 -val identity = morphism {binding = I, var = I, typ = I, term = I, fact = I};
    1.57 +val identity = morphism {binding = I, typ = I, term = I, fact = I};
    1.58  
    1.59  fun compose
    1.60 -    (Morphism {binding = binding1, var = var1, typ = typ1, term = term1, fact = fact1})
    1.61 -    (Morphism {binding = binding2, var = var2, typ = typ2, term = term2, fact = fact2}) =
    1.62 -  morphism {binding = binding1 o binding2, var = var1 o var2,
    1.63 -    typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2};
    1.64 +    (Morphism {binding = binding1, typ = typ1, term = term1, fact = fact1})
    1.65 +    (Morphism {binding = binding2, typ = typ2, term = term2, fact = fact2}) =
    1.66 +  morphism {binding = binding1 o binding2, typ = typ1 o typ2,
    1.67 +    term = term1 o term2, fact = fact1 o fact2};
    1.68  
    1.69  fun phi1 $> phi2 = compose phi2 phi1;
    1.70