1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Wed Sep 01 16:15:13 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Wed Sep 01 16:43:58 2010 +0200
     1.3 @@ -28,6 +28,8 @@
     1.4          (c) by Richard Lang, 2003 *}
     1.5  
     1.6  ML {*
     1.7 +val thy = @{theory};
     1.8 +
     1.9  val univariate_equation_prls = 
    1.10      append_rls "univariate_equation_prls" e_rls 
    1.11  	       [Calc ("Tools.matches",eval_matches "")];
    1.12 @@ -38,7 +40,7 @@
    1.13  
    1.14  
    1.15  store_pbt 
    1.16 - (prep_pbt (theory "Equation") "pbl_equ" [] e_pblID
    1.17 + (prep_pbt thy "pbl_equ" [] e_pblID
    1.18   (["equation"],
    1.19    [("#Given" ,["equality e_","solveFor v_"]),
    1.20     ("#Where" ,["matches (?a = ?b) e_"]),
    1.21 @@ -50,7 +52,7 @@
    1.22    []));
    1.23  
    1.24  store_pbt
    1.25 - (prep_pbt (theory "Equation") "pbl_equ_univ" [] e_pblID
    1.26 + (prep_pbt thy "pbl_equ_univ" [] e_pblID
    1.27   (["univariate","equation"],
    1.28    [("#Given" ,["equality e_","solveFor v_"]),
    1.29     ("#Where" ,["matches (?a = ?b) e_"]),
    1.30 @@ -86,7 +88,7 @@
    1.31  
    1.32  
    1.33  store_met
    1.34 -    (prep_met (theory "Equation") "met_equ" [] e_metID
    1.35 +    (prep_met thy "met_equ" [] e_metID
    1.36  	      (["Equation"],
    1.37  	       [],
    1.38  	       {rew_ord'="tless_true", rls'=Erls, calc = [],