src/ZF/Tools/typechk.ML
changeset 20193 46f5ef758422
parent 18736 541d04c79e12
child 21506 b2a673894ce5
equal deleted inserted replaced
20192:956cd30ef3be 20193:46f5ef758422
    48   type T = tcset
    48   type T = tcset
    49   val empty = TC {rules = [], net = Net.empty};
    49   val empty = TC {rules = [], net = Net.empty};
    50   val extend = I;
    50   val extend = I;
    51 
    51 
    52   fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
    52   fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
    53     TC {rules = gen_union Drule.eq_thm_prop (rules, rules'),
    53     TC {rules = Drule.merge_rules (rules, rules'),
    54         net = Net.merge Drule.eq_thm_prop (net, net')};
    54         net = Net.merge Drule.eq_thm_prop (net, net')};
    55 
    55 
    56   fun print context (TC {rules, ...}) =
    56   fun print context (TC {rules, ...}) =
    57     Pretty.writeln (Pretty.big_list "type-checking rules:"
    57     Pretty.writeln (Pretty.big_list "type-checking rules:"
    58       (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
    58       (map (ProofContext.pretty_thm (Context.proof_of context)) rules));