src/Pure/goals.ML
changeset 1580 e3fd931e6095
parent 1565 70dd38777109
child 1628 60136fdd80c4
equal deleted inserted replaced
1579:688e18023915 1580:e3fd931e6095
   309 fun by_com tac ((th,ths), pairs) : gstack =
   309 fun by_com tac ((th,ths), pairs) : gstack =
   310   (case  Sequence.pull(tac th)  of
   310   (case  Sequence.pull(tac th)  of
   311      None      => error"by: tactic failed"
   311      None      => error"by: tactic failed"
   312    | Some(th2,ths2) => 
   312    | Some(th2,ths2) => 
   313        (if eq_thm(th,th2) 
   313        (if eq_thm(th,th2) 
   314 	  then writeln"Warning: same as previous level"
   314 	  then warning "same as previous level"
   315 	  else if eq_thm_sg(th,th2) then ()
   315 	  else if eq_thm_sg(th,th2) then ()
   316 	  else writeln("Warning: signature of proof state has changed" ^
   316 	  else warning("signature of proof state has changed" ^
   317 		       sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
   317 		       sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
   318        ((th2,ths2)::(th,ths)::pairs)));
   318        ((th2,ths2)::(th,ths)::pairs)));
   319 
   319 
   320 fun by tac = cond_timeit (!proof_timing) 
   320 fun by tac = cond_timeit (!proof_timing) 
   321     (fn() => make_command (by_com tac));
   321     (fn() => make_command (by_com tac));
   331   | backtrack ((th,thstr) :: pairs) =
   331   | backtrack ((th,thstr) :: pairs) =
   332      (case Sequence.pull thstr of
   332      (case Sequence.pull thstr of
   333 	  None      => (writeln"Going back a level..."; backtrack pairs)
   333 	  None      => (writeln"Going back a level..."; backtrack pairs)
   334 	| Some(th2,thstr2) =>  
   334 	| Some(th2,thstr2) =>  
   335 	   (if eq_thm(th,th2) 
   335 	   (if eq_thm(th,th2) 
   336 	      then writeln"Warning: same as previous choice at this level"
   336 	      then warning "same as previous choice at this level"
   337 	      else if eq_thm_sg(th,th2) then ()
   337 	      else if eq_thm_sg(th,th2) then ()
   338 	      else writeln"Warning: signature of proof state has changed";
   338 	      else warning "signature of proof state has changed";
   339 	    (th2,thstr2)::pairs));
   339 	    (th2,thstr2)::pairs));
   340 
   340 
   341 fun back() = setstate (backtrack (getstate()));
   341 fun back() = setstate (backtrack (getstate()));
   342 
   342 
   343 (*Chop back to previous level of the proof*)
   343 (*Chop back to previous level of the proof*)