# HG changeset patch
# User nipkow
# Date 797494393 -7200
# Node ID f5f36bdc80033a491dfb8252574a0f16aa6e0948
# Parent  c4921e635bf7b125164aae676feea8556277209c
Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that
the maxidx-filed of thms is computed correctly.

diff -r c4921e635bf7 -r f5f36bdc8003 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Apr 07 10:12:01 1995 +0200
+++ b/src/Pure/thm.ML	Mon Apr 10 08:13:13 1995 +0200
@@ -1066,10 +1066,12 @@
 
 (*simple test for looping rewrite*)
 fun loops sign prems (lhs,rhs) =
-  is_Var(lhs) orelse
-  (is_Free(lhs) andalso (exists (apl(lhs, Logic.occs)) (rhs::prems))) orelse
-  (null(prems) andalso
-   Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs));
+   is_Var(lhs)
+  orelse
+   (exists (apl(lhs, Logic.occs)) (rhs::prems))
+  orelse
+   (null(prems) andalso
+    Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs));
 
 fun mk_rrule (thm as Thm{hyps,sign,prop,maxidx,...}) =
   let val prems = Logic.strip_imp_prems prop
@@ -1230,7 +1232,8 @@
             val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (lhs,etat)
             val prop' = ren_inst(insts,prop,lhs,t);
             val hyps' = hyps union hypst;
-            val thm' = Thm{sign=signt, hyps=hyps', prop=prop', maxidx=maxidx}
+            val thm' = Thm{sign=signt, hyps=hyps', prop=prop',
+                           maxidx=maxidx_of_term prop'}
             val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop')
         in if perm andalso not(termless(rhs',lhs')) then None else
            if Logic.count_prems(prop',0) = 0
@@ -1261,7 +1264,7 @@
                   error("Congruence rule did not match")
       val prop' = ren_inst(insts,prop,lhs,t);
       val thm' = Thm{sign=signt, hyps=hyps union hypst,
-                     prop=prop', maxidx=maxidx}
+                     prop=prop', maxidx=maxidx_of_term prop'}
       val unit = trace_thm "Applying congruence rule" thm';
       fun err() = error("Failed congruence proof!")