equal
deleted
inserted
replaced
120 val thy = Thm.theory_of_thm genth; |
120 val thy = Thm.theory_of_thm genth; |
121 |
121 |
122 (* check if we are a member of splitths - FIXME: quicker and |
122 (* check if we are a member of splitths - FIXME: quicker and |
123 more flexible with discrim net. *) |
123 more flexible with discrim net. *) |
124 fun solve_by_splitth th split = |
124 fun solve_by_splitth th split = |
125 Thm.biresolution false [(false,split)] 1 th; |
125 Thm.biresolution (SOME ctxt) false [(false,split)] 1 th; |
126 |
126 |
127 fun split th = |
127 fun split th = |
128 (case find_thms_split splitths 1 th of |
128 (case find_thms_split splitths 1 th of |
129 NONE => |
129 NONE => |
130 (writeln (cat_lines |
130 (writeln (cat_lines |