equal
deleted
inserted
replaced
10 val _ = |
10 val _ = |
11 ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context); |
11 ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context); |
12 |
12 |
13 val _ = |
13 val _ = |
14 ML_system_pp (fn depth => fn _ => |
14 ML_system_pp (fn depth => fn _ => |
15 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Thy_Info.pure_theory); |
15 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Theory.get_pure); |
16 |
16 |
17 val _ = |
17 val _ = |
18 ML_system_pp (fn depth => fn _ => |
18 ML_system_pp (fn depth => fn _ => |
19 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Thy_Info.pure_theory); |
19 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Theory.get_pure); |
20 |
20 |
21 val _ = |
21 val _ = |
22 ML_system_pp (fn depth => fn _ => |
22 ML_system_pp (fn depth => fn _ => |
23 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Thy_Info.pure_theory); |
23 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Theory.get_pure); |
24 |
24 |
25 val _ = |
25 val _ = |
26 ML_system_pp (fn depth => fn _ => |
26 ML_system_pp (fn depth => fn _ => |
27 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Thy_Info.pure_theory); |
27 ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure); |
28 |
28 |
29 |
29 |
30 local |
30 local |
31 |
31 |
32 fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt]; |
32 fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt]; |