1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Thu Jun 10 12:23:57 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Thu Jun 10 12:48:50 2021 +0200
     1.3 @@ -385,7 +385,7 @@
     1.4  \<close>
     1.5  
     1.6  section \<open>Embed cancellation and addition into rewriting\<close>
     1.7 -ML \<open>val thy = @{theory}\<close>
     1.8 +
     1.9  subsection \<open>Rulesets and predicate for embedding\<close>
    1.10  ML \<open>
    1.11  (* evaluates conditions in calculate_Rational *)
    1.12 @@ -510,7 +510,7 @@
    1.13  
    1.14  val cancel_p = 
    1.15    Rule_Set.Rrls {id = "cancel_p", prepat = [],
    1.16 -	rew_ord=("ord_make_polynomial", ord_make_polynomial false thy),
    1.17 +	rew_ord=("ord_make_polynomial", ord_make_polynomial false \<^theory>),
    1.18  	erls = rational_erls, 
    1.19  	calc = 
    1.20  	  [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
    1.21 @@ -519,10 +519,10 @@
    1.22  	  ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))],
    1.23      errpatts = [],
    1.24  	scr =
    1.25 -	  Rule.Rfuns {init_state  = init_state thy Atools_erls ro,
    1.26 -		normal_form = cancel_p_ thy, 
    1.27 -		locate_rule = locate_rule thy Atools_erls ro,
    1.28 -		next_rule   = next_rule thy Atools_erls ro,
    1.29 +	  Rule.Rfuns {init_state  = init_state \<^theory> Atools_erls ro,
    1.30 +		normal_form = cancel_p_ \<^theory>, 
    1.31 +		locate_rule = locate_rule \<^theory> Atools_erls ro,
    1.32 +		next_rule   = next_rule \<^theory> Atools_erls ro,
    1.33  		attach_form = attach_form}}
    1.34  (**)end(* local cancel_p *)
    1.35  \<close>
    1.36 @@ -568,9 +568,9 @@
    1.37      end
    1.38    | next_rule _ _ _ _ _ = raise ERROR ("next_rule: doesnt match rev-sets in istate");
    1.39  
    1.40 -val pat0 = TermC.parse_patt thy "?r/?s+?u/?v :: real";
    1.41 -val pat1 = TermC.parse_patt thy "?r/?s+?u    :: real";
    1.42 -val pat2 = TermC.parse_patt thy "?r   +?u/?v :: real";
    1.43 +val pat0 = TermC.parse_patt \<^theory> "?r/?s+?u/?v :: real";
    1.44 +val pat1 = TermC.parse_patt \<^theory> "?r/?s+?u    :: real";
    1.45 +val pat2 = TermC.parse_patt \<^theory> "?r   +?u/?v :: real";
    1.46  val prepat = [([@{term True}], pat0),
    1.47  	      ([@{term True}], pat1),
    1.48  	      ([@{term True}], pat2)];
    1.49 @@ -578,17 +578,17 @@
    1.50  
    1.51  val add_fractions_p =
    1.52    Rule_Set.Rrls {id = "add_fractions_p", prepat=prepat,
    1.53 -    rew_ord = ("ord_make_polynomial", ord_make_polynomial false thy),
    1.54 +    rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
    1.55      erls = rational_erls,
    1.56      calc = [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
    1.57        ("TIMES", ("Groups.times_class.times", (**)eval_binop "#mult_")),
    1.58        ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
    1.59        ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))],
    1.60      errpatts = [],
    1.61 -    scr = Rule.Rfuns {init_state  = init_state thy Atools_erls ro,
    1.62 -      normal_form = add_fraction_p_ thy,
    1.63 -      locate_rule = locate_rule thy Atools_erls ro,
    1.64 -      next_rule   = next_rule thy Atools_erls ro,
    1.65 +    scr = Rule.Rfuns {init_state  = init_state \<^theory> Atools_erls ro,
    1.66 +      normal_form = add_fraction_p_ \<^theory>,
    1.67 +      locate_rule = locate_rule \<^theory> Atools_erls ro,
    1.68 +      next_rule   = next_rule \<^theory> Atools_erls ro,
    1.69        attach_form = attach_form}}
    1.70  (**)end(*local add_fractions_p *)
    1.71  \<close>