src/Provers/blast.ML
changeset 14913 e993eabc7197
parent 14466 b737e523fc6c
child 14984 edbc81e60809
equal deleted inserted replaced
14912:88b9d9165452 14913:e993eabc7197
   625 	  None   => stm   (*no type to attach*)
   625 	  None   => stm   (*no type to attach*)
   626 	| Some T => stm ^ "\t:: " ^ Sign.string_of_typ sign T
   626 	| Some T => stm ^ "\t:: " ^ Sign.string_of_typ sign T
   627   end;
   627   end;
   628 
   628 
   629 
   629 
   630 val prs = std_output;
   630 val prs = std_output o Output.output;
   631 
   631 
   632 (*Print tracing information at each iteration of prover*)
   632 (*Print tracing information at each iteration of prover*)
   633 fun tracing sign brs = 
   633 fun tracing sign brs = 
   634   let fun printPairs (((G,_)::_,_)::_)  = prs(traceTerm sign G)
   634   let fun printPairs (((G,_)::_,_)::_)  = prs(traceTerm sign G)
   635 	| printPairs (([],(H,_)::_)::_) = prs(traceTerm sign H ^ "\t (Unsafe)")
   635 	| printPairs (([],(H,_)::_)::_) = prs(traceTerm sign H ^ "\t (Unsafe)")