src/Pure/thm.ML

 fun var_perm(t,u) = vperm(t,u) andalso
                     eq_set(add_term_vars(t,[]), add_term_vars(u,[]))
 
 (*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
       val concl = Logic.strip_imp_concl prop
       val (lhs,_) = Logic.dest_equals concl handle TERM _ =>

                           thm;
                         raise Pattern.MATCH)
             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
            then (trace_thm "Rewriting:" thm'; Some(hyps',rhs'))
            else (trace_thm "Trying to rewrite:" thm';

       val tsig = #tsig(Sign.rep_sg signt)
       val insts = Pattern.match tsig (lhs,t) handle Pattern.MATCH =>
                   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!")
 
   in case prover thm' of
        None => err()