29 toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy"; |
29 toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy"; |
30 toplevel_pp ["Context", "theory"] "Context.pretty_thy"; |
30 toplevel_pp ["Context", "theory"] "Context.pretty_thy"; |
31 toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref"; |
31 toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref"; |
32 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; |
32 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; |
33 toplevel_pp ["Ast", "ast"] "Ast.pretty_ast"; |
33 toplevel_pp ["Ast", "ast"] "Ast.pretty_ast"; |
34 toplevel_pp ["Path", "T"] "Pretty.str o Path.print"; |
34 toplevel_pp ["Path", "T"] "Path.pretty"; |
35 toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep"; |
35 toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep"; |
36 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")"; |
36 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")"; |
37 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract"; |
37 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract"; |
38 |
38 |
39 if ml_system = "polyml-5.2.1" |
39 if ml_system = "polyml-5.2.1" |