equal
deleted
inserted
replaced
622 val clauses = make_clauses [thm] |
622 val clauses = make_clauses [thm] |
623 val numcls = zip (numlist (length clauses)) (map make_meta_clause clauses) |
623 val numcls = zip (numlist (length clauses)) (map make_meta_clause clauses) |
624 |
624 |
625 in |
625 in |
626 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
626 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
627 apply_res_thm reconstr goalstring; |
627 Recon_Transfer.apply_res_thm reconstr goalstring; |
628 Pretty.writeln(Pretty.str (oct_char "361")); |
628 Pretty.writeln(Pretty.str (oct_char "361")); |
629 killWatcher childpid; () |
629 killWatcher childpid; () |
630 end |
630 end |
631 else |
631 else |
632 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
632 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
649 if ( (substring (reconstr, 0,1))= "[") |
649 if ( (substring (reconstr, 0,1))= "[") |
650 then |
650 then |
651 |
651 |
652 ( |
652 ( |
653 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
653 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
654 apply_res_thm reconstr goalstring; |
654 Recon_Transfer.apply_res_thm reconstr goalstring; |
655 Pretty.writeln(Pretty.str (oct_char "361")); |
655 Pretty.writeln(Pretty.str (oct_char "361")); |
656 |
656 |
657 goals_being_watched := ((!goals_being_watched) - 1); |
657 goals_being_watched := ((!goals_being_watched) - 1); |
658 |
658 |
659 if ((!goals_being_watched) = 0) |
659 if ((!goals_being_watched) = 0) |