src/Pure/morphism.ML
changeset 62663 bea354f6ff21
parent 62505 9e2a65912111
child 62819 d3ff367a16a0
equal deleted inserted replaced
62662:291cc01f56f5 62663:bea354f6ff21
    69 
    69 
    70 type declaration = morphism -> Context.generic -> Context.generic;
    70 type declaration = morphism -> Context.generic -> Context.generic;
    71 
    71 
    72 fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names));
    72 fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names));
    73 
    73 
       
    74 val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty);
       
    75 
    74 fun binding (Morphism {binding, ...}) = apply binding;
    76 fun binding (Morphism {binding, ...}) = apply binding;
    75 fun typ (Morphism {typ, ...}) = apply typ;
    77 fun typ (Morphism {typ, ...}) = apply typ;
    76 fun term (Morphism {term, ...}) = apply term;
    78 fun term (Morphism {term, ...}) = apply term;
    77 fun fact (Morphism {fact, ...}) = apply fact;
    79 fun fact (Morphism {fact, ...}) = apply fact;
    78 val thm = singleton o fact;
    80 val thm = singleton o fact;