equal
deleted
inserted
replaced
1348 |> Thm.adjust_maxidx_cterm ~1; |
1348 |> Thm.adjust_maxidx_cterm ~1; |
1349 val maxidx = Thm.maxidx_of_cterm ct; |
1349 val maxidx = Thm.maxidx_of_cterm ct; |
1350 |
1350 |
1351 val ctxt = |
1351 val ctxt = |
1352 raw_ctxt |
1352 raw_ctxt |
|
1353 |> Variable.set_body true |
1353 |> Context_Position.set_visible false |
1354 |> Context_Position.set_visible false |
1354 |> inc_simp_depth |
1355 |> inc_simp_depth |
1355 |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = Thm.term_of ct} ctxt); |
1356 |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = Thm.term_of ct} ctxt); |
1356 |
1357 |
1357 val _ = |
1358 val _ = |