1.1 --- a/src/sml/Scripts/calculate.sml	Sat Aug 20 15:15:41 2005 +0200
     1.2 +++ b/src/sml/Scripts/calculate.sml	Sat Aug 20 15:15:41 2005 +0200
     1.3 @@ -83,34 +83,27 @@
     1.4         (thy,op_,eval_fn,ct);
     1.5     *)
     1.6    | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2)) =  (* binary funs*)
     1.7 -    ((*writeln("@@@ get_pair: binop, t = "^
     1.8 -	     (Sign.string_of_term (sign_of thy) t));*)
     1.9 +    ((*writeln("1.. get_pair: binop = "^op_);*)
    1.10       if op_ = op0 then 
    1.11 -	 let (*val _=writeln"@@@ get_pair: then 1"*)
    1.12 -	     val popt = ef op_ t thy
    1.13 -	 (*val _ = writeln("@@@ get_pair: "^term2str t^" -> "^popt2str popt)*)
    1.14 +	 let val popt = ef op_ t thy
    1.15 +	 (*val _ = writeln("2.. get_pair: "^term2str t^" -> "^popt2str popt)*)
    1.16  	 in case popt of 
    1.17  		Some (id,_) => popt
    1.18  	      | None => 
    1.19  		let val popt = get_pair thy op_ ef t1
    1.20 -		    (*val _ = writeln("@@@ get_pair: "^term2str t1^
    1.21 +		    (*val _ = writeln("3.. get_pair: "^term2str t1^
    1.22  				    " -> "^popt2str popt)*)
    1.23  		in case popt of 
    1.24 -		       Some (id,_) => 
    1.25 -		       ((*writeln("@@@ get_pair: t1 -> Some "^id);*)
    1.26 -			popt)
    1.27 -		     | None => ((*writeln"@@@ get_pair: t1 -> None";*)
    1.28 -				get_pair thy op_ ef t2) 
    1.29 +		       Some (id,_) => popt
    1.30 +		     | None => get_pair thy op_ ef t2
    1.31  		end
    1.32  	 end
    1.33       else (*search subterms*)
    1.34 -	 let (*val _= writeln"@@@ get_pair: t else"*)
    1.35 -	     val popt = get_pair thy op_ ef t1
    1.36 +	 let val popt = get_pair thy op_ ef t1
    1.37 +	 (*val _ = writeln("4.. get_pair: "^term2str t^" -> "^popt2str popt)*)
    1.38  	 in case popt of 
    1.39 -		Some (id,_) => ((*writeln("@@@ get_pair: t1 -> Some "^id);*)
    1.40 -				popt)
    1.41 -	      | None => ((*writeln"@@@ get_pair: t1 else -> None";*)
    1.42 -			 get_pair thy op_ ef t2) 
    1.43 +		Some (id,_) => popt
    1.44 +	      | None => get_pair thy op_ ef t2
    1.45  	 end)
    1.46  
    1.47    | get_pair thy op_ ef (Const _) = None
    1.48 @@ -119,8 +112,8 @@
    1.49    | get_pair thy op_ ef (Bound _) = None
    1.50    | get_pair thy op_ ef (Abs(a,T,body)) = get_pair thy op_ ef body
    1.51    | get_pair thy op_ ef (t1$t2) = 
    1.52 -    let (*val _= writeln("### get_pair t1 $ t2: "^term2str t1^" 
    1.53 -						    $ "^term2str t2)*)
    1.54 +    let(*val _= writeln("5.. get_pair t1 $ t2: "^term2str t1^" 
    1.55 +						   $ "^term2str t2)*)
    1.56  	val popt = get_pair thy op_ ef t1
    1.57      in case popt of 
    1.58  	   Some _ => popt