equal
deleted
inserted
replaced
93 val type_sys = |
93 val type_sys = |
94 ATP_Translate.Preds |
94 ATP_Translate.Preds |
95 (ATP_Translate.Polymorphic, |
95 (ATP_Translate.Polymorphic, |
96 if full_types then ATP_Translate.All_Types |
96 if full_types then ATP_Translate.All_Types |
97 else ATP_Translate.Const_Arg_Types, |
97 else ATP_Translate.Const_Arg_Types, |
98 ATP_Translate.Heavy) |
98 ATP_Translate.Heavyweight) |
99 val path = file_name |> Path.explode |
99 val path = file_name |> Path.explode |
100 val _ = File.write path "" |
100 val _ = File.write path "" |
101 val facts0 = facts_of thy |
101 val facts0 = facts_of thy |
102 val facts = |
102 val facts = |
103 facts0 |> map_filter (try (fn ((_, loc), (_, th)) => |
103 facts0 |> map_filter (try (fn ((_, loc), (_, th)) => |