equal
deleted
inserted
replaced
121 |> adjust_type_enc format |
121 |> adjust_type_enc format |
122 val mono = not (is_type_enc_polymorphic type_enc) |
122 val mono = not (is_type_enc_polymorphic type_enc) |
123 val path = file_name |> Path.explode |
123 val path = file_name |> Path.explode |
124 val _ = File.write path "" |
124 val _ = File.write path "" |
125 val facts = |
125 val facts = |
126 Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table |
126 Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) false |
|
127 Symtab.empty [] [] css_table |
127 val atp_problem = |
128 val atp_problem = |
128 facts |
129 facts |
129 |> map (fn ((_, loc), th) => |
130 |> map (fn ((_, loc), th) => |
130 ((Thm.get_name_hint th, loc), |
131 ((Thm.get_name_hint th, loc), |
131 th |> prop_of |> mono ? monomorphize_term ctxt)) |
132 th |> prop_of |> mono ? monomorphize_term ctxt)) |