1.1 --- a/src/Tools/isac/Knowledge/Atools.thy	Mon Jul 28 17:06:16 2014 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy	Thu Jul 31 14:15:41 2014 +0200
     1.3 @@ -259,7 +259,7 @@
     1.4  		(*WN071229 "Fields.inverse_class.divide" never tried*)
     1.5  		val rhs = var_op_float v op_ t0 T1 res
     1.6  		val prop = Trueprop $ (mk_equality (t, rhs))
     1.7 -	    in SOME (mk_thmid_f thmid n1 n2, prop) end
     1.8 +	    in SOME ("#: " ^ term2str prop, prop) end
     1.9  	  | _ => NONE
    1.10      else NONE
    1.11    | eval_binop (thmid:string) (op_:string) 
    1.12 @@ -275,7 +275,7 @@
    1.13  		val res = calc op0 n1 n2
    1.14  		val rhs = float_op_var v op_ t0 T1 res
    1.15  		val prop = Trueprop $ (mk_equality (t, rhs))
    1.16 -	    in SOME (mk_thmid_f thmid n1 n2, prop) end
    1.17 +	    in SOME ("#: " ^ term2str prop, prop) end
    1.18  	  | _ => NONE
    1.19    else NONE
    1.20      
    1.21 @@ -287,7 +287,7 @@
    1.22  	     val res = calc op0 n1 n2;
    1.23  	     val rhs = term_of_float Trange res;
    1.24  	     val prop = Trueprop $ (mk_equality (t, rhs));
    1.25 -	 in SOME (mk_thmid_f thmid n1 n2, prop) end
    1.26 +	 in SOME ("#: " ^ term2str prop, prop) end
    1.27         | _ => NONE)
    1.28    | eval_binop _ _ _ _ = NONE; 
    1.29  (*