# HG changeset patch
# User berghofe
# Date 1027520204 -7200
# Node ID 12cc77f90811835606946dc78d1059ee729a0e5b
# Parent  5851987ab2e805ff9168e5d9833ecd0586684b00
Tuned type constraint of function merge_rules to make smlnj happy.

diff -r 5851987ab2e8 -r 12cc77f90811 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Wed Jul 24 00:13:41 2002 +0200
+++ b/src/Pure/Proof/extraction.ML	Wed Jul 24 16:16:44 2002 +0200
@@ -80,8 +80,8 @@
   {next = next - 1, rs = r :: rs, net = Net.insert_term
      ((Pattern.eta_contract lhs, (next, r)), net, K false)};
 
-fun (merge_rules : rules -> rules -> rules)
-  {next, rs = rs1, net} {next = next2, rs = rs2, ...} =
+fun merge_rules
+  ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
   foldr add_rule (rs2 \\ rs1, {next = next, rs = rs1, net = net});
 
 fun condrew sign rules procs =
@@ -618,7 +618,6 @@
               (fst (Proofterm.freeze_thaw_prf (ProofRewriteRules.rewrite_terms
                 (Pattern.rewrite_term (Sign.tsig_of (sign_of thy)) []
                   [rlz_proc']) prf)))))), []) thy)
-      | add_thm (_, thy) = thy
 
   in thy |>
     Theory.absolute_path |>