1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Sun Oct 14 14:43:41 2012 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Sun Oct 14 20:00:27 2012 +0200
     1.3 @@ -342,7 +342,7 @@
     1.4  	      (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
     1.5         Thm("sqrt_square_equation_right_6",num_str @{thm sqrt_square_equation_right_6})
     1.6  	      (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
     1.7 -       ],scr = Script ((term_of o the o (parse thy)) "empty_script")
     1.8 +       ],scr = Prog ((term_of o the o (parse thy)) "empty_script")
     1.9        }:rls);
    1.10  
    1.11  ruleset' := overwritelthy @{theory} (!ruleset',
    1.12 @@ -390,7 +390,7 @@
    1.13       Thm("sqrt_square_equation_left_6",num_str @{thm sqrt_square_equation_left_6})  
    1.14  	      (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
    1.15      ],
    1.16 -    scr = Script ((term_of o the o (parse thy)) "empty_script")
    1.17 +    scr = Prog ((term_of o the o (parse thy)) "empty_script")
    1.18     }:rls);
    1.19  
    1.20  ruleset' := overwritelthy @{theory} (!ruleset',
    1.21 @@ -439,7 +439,7 @@
    1.22       Thm("sqrt_square_equation_right_6",num_str @{thm sqrt_square_equation_right_6})
    1.23  	      (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
    1.24      ],
    1.25 -    scr = Script ((term_of o the o (parse thy)) "empty_script")
    1.26 +    scr = Prog ((term_of o the o (parse thy)) "empty_script")
    1.27     }:rls);
    1.28  
    1.29  ruleset' := overwritelthy @{theory} (!ruleset',
    1.30 @@ -474,7 +474,7 @@
    1.31                  Thm("sqrt_square_1",num_str @{thm sqrt_square_1}) 
    1.32                              (* sqrt a ^^^ 2 = a *)
    1.33                  ],
    1.34 -       scr = Script ((term_of o the o (parse thy)) "empty_script")
    1.35 +       scr = Prog ((term_of o the o (parse thy)) "empty_script")
    1.36      }:rls);
    1.37    ruleset' := overwritelthy @{theory} (!ruleset',
    1.38                            [("rooteq_simplify",rooteq_simplify)