equal
deleted
inserted
replaced
300 |
300 |
301 fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t = |
301 fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t = |
302 let |
302 let |
303 val names = Term.declare_term_names t Name.context; |
303 val names = Term.declare_term_names t Name.context; |
304 val xs = rev (#1 (fold_map Name.variant (rev (map #2 bs)) names)); |
304 val xs = rev (#1 (fold_map Name.variant (rev (map #2 bs)) names)); |
305 fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_boundT (x', T)); |
305 fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_bound_abs (x', T)); |
306 in Term.subst_atomic (ListPair.map subst (bs, xs)) t end; |
306 in Term.subst_atomic (ListPair.map subst (bs, xs)) t end; |
307 |
307 |
308 fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^ |
308 fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^ |
309 Syntax.string_of_term ctxt |
309 Syntax.string_of_term ctxt |
310 (if Config.get ctxt simp_debug then t else show_bounds ss t)); |
310 (if Config.get ctxt simp_debug then t else show_bounds ss t)); |