src/Pure/ROOT.ML
changeset 62356 e307a410f46c
parent 62355 00f7618a9f2b
child 62359 6709e51d5c11
     1.1 --- a/src/Pure/ROOT.ML	Wed Feb 17 23:15:47 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Wed Feb 17 23:28:58 2016 +0100
     1.3 @@ -47,8 +47,6 @@
     1.4        Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
     1.5          handle ERROR msg => (writeln msg; error "ML error")) ();
     1.6  
     1.7 -val toplevel_pp = Secure.toplevel_pp;
     1.8 -
     1.9  
    1.10  
    1.11  (** bootstrap phase 1: towards ML within Isar context *)
    1.12 @@ -333,27 +331,6 @@
    1.13  structure Output: OUTPUT = Output;  (*seal system channels!*)
    1.14  
    1.15  
    1.16 -(* ML toplevel pretty printing *)
    1.17 -
    1.18 -toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
    1.19 -toplevel_pp ["Scan", "lexicon"] "Lexicon.pp_lexicon";
    1.20 -toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
    1.21 -toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
    1.22 -toplevel_pp ["Position", "T"] "Pretty.position";
    1.23 -toplevel_pp ["Binding", "binding"] "Binding.pp";
    1.24 -toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm Thy_Info.pure_theory";
    1.25 -toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm Thy_Info.pure_theory";
    1.26 -toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp Thy_Info.pure_theory";
    1.27 -toplevel_pp ["typ"] "Proof_Display.pp_typ Thy_Info.pure_theory";
    1.28 -toplevel_pp ["Context", "theory"] "Context.pretty_thy";
    1.29 -toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
    1.30 -toplevel_pp ["Ast", "ast"] "Ast.pretty_ast";
    1.31 -toplevel_pp ["Path", "T"] "Path.pretty";
    1.32 -toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
    1.33 -toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
    1.34 -toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
    1.35 -toplevel_pp ["Morphism", "morphism"] "Morphism.pretty";
    1.36 -
    1.37  use "ML/install_pp_polyml.ML";
    1.38  
    1.39