changeset 19052 | 113dbd65319e |
parent 18929 | d81435108688 |
child 19142 | 99a72b8c9974 |
--- a/src/Pure/meta_simplifier.ML Wed Feb 15 21:35:02 2006 +0100 +++ b/src/Pure/meta_simplifier.ML Wed Feb 15 21:35:02 2006 +0100 @@ -1157,8 +1157,9 @@ (Thm.theory_of_cterm ct) (Thm.term_of ct) end); -fun rewrite_cterm mode prover raw_ss ct = +fun rewrite_cterm mode prover raw_ss raw_ct = let + val ct = Thm.adjust_maxidx raw_ct; val {thy, t, maxidx, ...} = Thm.rep_cterm ct; val ss = fallback_context thy raw_ss; val _ = inc simp_depth;