equal
deleted
inserted
replaced
16 Thy_Info.register_theory Pure.thy; |
16 Thy_Info.register_theory Pure.thy; |
17 |
17 |
18 |
18 |
19 (* ML toplevel pretty printing *) |
19 (* ML toplevel pretty printing *) |
20 |
20 |
21 toplevel_pp ["String", "string"] "ML_Syntax.pretty_string"; |
21 if String.isPrefix "smlnj" ml_system then () |
|
22 else toplevel_pp ["String", "string"] "ML_Syntax.pretty_string"; |
|
23 |
22 toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")"; |
24 toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")"; |
23 toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task"; |
25 toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task"; |
24 toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group"; |
26 toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group"; |
25 toplevel_pp ["Position", "T"] "Pretty.position"; |
27 toplevel_pp ["Position", "T"] "Pretty.position"; |
26 toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of"; |
28 toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of"; |