Tuned type constraint of function merge_rules to make smlnj happy.
authorberghofe
Wed Jul 24 16:16:44 2002 +0200 (2002-07-24)
changeset 1341712cc77f90811
parent 13416 5851987ab2e8
child 13418 7c0ba9dba978
Tuned type constraint of function merge_rules to make smlnj happy.
src/Pure/Proof/extraction.ML
     1.1 --- a/src/Pure/Proof/extraction.ML	Wed Jul 24 00:13:41 2002 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Wed Jul 24 16:16:44 2002 +0200
     1.3 @@ -80,8 +80,8 @@
     1.4    {next = next - 1, rs = r :: rs, net = Net.insert_term
     1.5       ((Pattern.eta_contract lhs, (next, r)), net, K false)};
     1.6  
     1.7 -fun (merge_rules : rules -> rules -> rules)
     1.8 -  {next, rs = rs1, net} {next = next2, rs = rs2, ...} =
     1.9 +fun merge_rules
    1.10 +  ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
    1.11    foldr add_rule (rs2 \\ rs1, {next = next, rs = rs1, net = net});
    1.12  
    1.13  fun condrew sign rules procs =
    1.14 @@ -618,7 +618,6 @@
    1.15                (fst (Proofterm.freeze_thaw_prf (ProofRewriteRules.rewrite_terms
    1.16                  (Pattern.rewrite_term (Sign.tsig_of (sign_of thy)) []
    1.17                    [rlz_proc']) prf)))))), []) thy)
    1.18 -      | add_thm (_, thy) = thy
    1.19  
    1.20    in thy |>
    1.21      Theory.absolute_path |>