equal
deleted
inserted
replaced
158 type_enc |> type_enc_of_string Non_Strict |
158 type_enc |> type_enc_of_string Non_Strict |
159 |> adjust_type_enc format |
159 |> adjust_type_enc format |
160 val mono = not (is_type_enc_polymorphic type_enc) |
160 val mono = not (is_type_enc_polymorphic type_enc) |
161 |
161 |
162 val facts = |
162 val facts = |
163 Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false |
163 Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true Keyword.empty_keywords [] [] |
164 Keyword.empty_keywords [] [] css_table |
164 css_table |
165 |> sort (Sledgehammer_MaSh.crude_thm_ord ctxt o apply2 snd) |
165 |> sort (Sledgehammer_MaSh.crude_thm_ord ctxt o apply2 snd) |
166 val problem = |
166 val problem = |
167 facts |
167 facts |
168 |> map (fn ((_, loc), th) => |
168 |> map (fn ((_, loc), th) => |
169 ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt)) |
169 ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt)) |