1.1 --- a/src/Tools/isac/IsacKnowledge/RatEq.ML	Wed Aug 18 13:53:15 2010 +0200
     1.2 +++ b/src/Tools/isac/IsacKnowledge/RatEq.ML	Wed Aug 18 13:55:23 2010 +0200
     1.3 @@ -36,11 +36,11 @@
     1.4      
     1.5  fun eval_is_ratequation_in _ _ (p as (Const ("RatEq.is'_ratequation'_in",_) $ t $ v)) _  =
     1.6      if is_rateqation_in t v then 
     1.7 -	Some ((term2str p) ^ " = True",
     1.8 +	SOME ((term2str p) ^ " = True",
     1.9  	      Trueprop $ (mk_equality (p, HOLogic.true_const)))
    1.10 -    else Some ((term2str p) ^ " = True",
    1.11 +    else SOME ((term2str p) ^ " = True",
    1.12  	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
    1.13 -  | eval_is_ratequation_in _ _ _ _ = ((*writeln"### nichts matcht";*) None);
    1.14 +  | eval_is_ratequation_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
    1.15  
    1.16  (*-------------------------rulse-----------------------*)
    1.17  val RatEq_prls = (*15.10.02:just the following order due to subterm evaluation*)
    1.18 @@ -156,7 +156,7 @@
    1.19     ("#Find"  ,["solutions v_i_"]) 
    1.20    ],
    1.21  
    1.22 -  RatEq_prls, Some "solve (e_::bool, v_)",
    1.23 +  RatEq_prls, SOME "solve (e_::bool, v_)",
    1.24    [["RatEq","solve_rat_equation"]]));
    1.25  
    1.26