equal
deleted
inserted
replaced
106 pretty_ffpairs tpairs @ |
106 pretty_ffpairs tpairs @ |
107 (if ! show_consts then pretty_consts prop else []) @ |
107 (if ! show_consts then pretty_consts prop else []) @ |
108 (if types then pretty_vars prop else []) @ |
108 (if types then pretty_vars prop else []) @ |
109 (if sorts then pretty_varsT prop else []); |
109 (if sorts then pretty_varsT prop else []); |
110 in |
110 in |
111 setmp show_no_free_types true |
111 setmp_CRITICAL show_no_free_types true |
112 (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types) |
112 (setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse ! show_all_types) |
113 (setmp show_sorts false pretty_gs)) |
113 (setmp_CRITICAL show_sorts false pretty_gs)) |
114 (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts) |
114 (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts) |
115 end; |
115 end; |
116 |
116 |
117 fun pretty_goals_without_context n th = |
117 fun pretty_goals_without_context n th = |
118 pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th)) |
118 pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th)) |