equal
deleted
inserted
replaced
241 end |
241 end |
242 handle ERROR mesg => simple_smart_string_of_cterm ct |
242 handle ERROR mesg => simple_smart_string_of_cterm ct |
243 |
243 |
244 val smart_string_of_thm = smart_string_of_cterm o cprop_of |
244 val smart_string_of_thm = smart_string_of_cterm o cprop_of |
245 |
245 |
246 fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm th) |
246 fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th) |
247 fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct) |
247 fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct) |
248 fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (the_context ()) t) ()); |
248 fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (the_context ()) t) ()); |
249 fun pth (HOLThm(ren,thm)) = |
249 fun pth (HOLThm(ren,thm)) = |
250 let |
250 let |
251 (*val _ = writeln "Renaming:" |
251 (*val _ = writeln "Renaming:" |