equal
deleted
inserted
replaced
246 val problem = |
246 val problem = |
247 {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, |
247 {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, |
248 facts = facts |> map (apfst (apfst (fn name => name ()))) |
248 facts = facts |> map (apfst (apfst (fn name => name ()))) |
249 |> map Untranslated_Fact} |
249 |> map Untranslated_Fact} |
250 in |
250 in |
251 get_minimizing_prover ctxt MaSh (K ()) prover params (K (K (K ""))) |
251 get_minimizing_prover ctxt MaSh (K (K ())) prover params (K (K (K ""))) |
252 problem |
252 problem |
253 end |
253 end |
254 |
254 |
255 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] |
255 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] |
256 |
256 |