1.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Wed Sep 01 16:15:13 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Wed Sep 01 16:43:58 2010 +0200
     1.3 @@ -49,6 +49,8 @@
     1.4     "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)"
     1.5  
     1.6  ML {*
     1.7 +val thy = @{theory};
     1.8 +
     1.9  (*-------------------------functions-----------------------*)
    1.10  (* is_rateqation_in becomes true, if a bdv is in the denominator of a fraction*)
    1.11  fun is_rateqation_in t v = 
    1.12 @@ -175,7 +177,7 @@
    1.13  show_ptyps(); 
    1.14  *)
    1.15  store_pbt
    1.16 - (prep_pbt (theory "RatEq") "pbl_equ_univ_rat" [] e_pblID
    1.17 + (prep_pbt thy "pbl_equ_univ_rat" [] e_pblID
    1.18   (["rational","univariate","equation"],
    1.19    [("#Given" ,["equality e_","solveFor v_"]),
    1.20     ("#Where" ,["(e_::bool) is_ratequation_in (v_::real)"]),
    1.21 @@ -188,14 +190,14 @@
    1.22  
    1.23  (*-------------------------methods-----------------------*)
    1.24  store_met
    1.25 - (prep_met (theory "RatEq") "met_rateq" [] e_metID
    1.26 + (prep_met thy "met_rateq" [] e_metID
    1.27   (["RatEq"],
    1.28     [],
    1.29     {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
    1.30      crls=RatEq_crls, nrls=norm_Rational
    1.31      (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
    1.32  store_met
    1.33 - (prep_met (theory "RatEq") "met_rat_eq" [] e_metID
    1.34 + (prep_met thy "met_rat_eq" [] e_metID
    1.35   (["RatEq","solve_rat_equation"],
    1.36     [("#Given" ,["equality e_","solveFor v_"]),
    1.37     ("#Where" ,["(e_::bool) is_ratequation_in (v_::real)"]),