1.1 --- a/src/Tools/isac/Knowledge/Test.sml	Wed Sep 08 16:45:27 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Test.sml	Wed Sep 08 16:47:22 2010 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  val ttt = (term_of o the o (parse thy))
     1.5 -"(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) e_e";
     1.6 +"(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e";
     1.7  val ttt = (term_of o the o (parse thy))
     1.8 -"(Try (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) e_e)";
     1.9 +"(Try (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e)";
    1.10  
    1.11  val ttt = (term_of o the o (parse thy))
    1.12   "(Rewrite_Set SqRoot_simplify False) e_e ";
    1.13 @@ -32,7 +32,7 @@
    1.14  val ttt = (term_of o the o (parse thy))
    1.15   "Script Solve_linear (e_e::bool) (v_v::real)=             \
    1.16   \(let e_e = \
    1.17 - \   (Repeat ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False)) e_e)\
    1.18 + \   (Repeat ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False)) e_e)\
    1.19   \ in [e_])";
    1.20  (*----*)
    1.21  val ttt = (term_of o the o (parse thy))
    1.22 @@ -42,7 +42,7 @@
    1.23   "Script Solve_linear (e_e::bool) (v_v::real)=             \
    1.24   \(let e_e = \
    1.25   \  (Repeat\
    1.26 - \    ((%ee_. (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_)\
    1.27 + \    ((%ee_. (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\
    1.28   \      e_e)\
    1.29   \    e_e)\
    1.30   \ in [e_])";
    1.31 @@ -51,7 +51,7 @@
    1.32   \(let e_e = \
    1.33   \  (Repeat\
    1.34   \    ((%ee_.\
    1.35 - \        ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_))\
    1.36 + \        ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_))\
    1.37   \      e_e)\
    1.38   \    e_e)\
    1.39   \ in [e_])";
    1.40 @@ -60,7 +60,7 @@
    1.41   \(let e_e = \
    1.42   \  (Repeat\
    1.43   \    ((%ee_.\
    1.44 - \        (let e_e = ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_)\
    1.45 + \        (let e_e = ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\
    1.46   \         in ((Rewrite_Set SqRoot_simplify False) e_e)) )\
    1.47   \      e_e)\
    1.48   \    e_e)\
    1.49 @@ -121,22 +121,22 @@
    1.50   "Script Solve_linear (e_e::bool) (v_v::real)=             \
    1.51   \(let e_e = \
    1.52   \  ((Repeat\
    1.53 - \    (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
    1.54 + \    (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
    1.55   \      (Rewrite_Set SqRoot_simplify False)))) e_e)\
    1.56   \ in [e_])";
    1.57  atomty ttt;
    1.58  
    1.59  
    1.60  val ttt = (term_of o the o (parse thy))
    1.61 -"(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@ yyy";
    1.62 +"(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ yyy";
    1.63  atomty ttt;
    1.64  val ttt = (term_of o the o (parse thy))
    1.65 - "(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
    1.66 + "(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
    1.67   \ (Rewrite_Set SqRoot_simplify False)";
    1.68  atomty ttt;
    1.69  val ttt = (term_of o the o (parse thy))
    1.70   "(Repeat\
    1.71 - \  ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
    1.72 + \  ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
    1.73   \  (Rewrite_Set SqRoot_simplify False))) e_e";
    1.74  atomty ttt;
    1.75  val ttt = (term_of o the o (parseold thy))
    1.76 @@ -150,7 +150,7 @@
    1.77   "Script Solve_linear (e_e::bool) (v_v::real)=             \
    1.78   \(let e_e =\
    1.79   \  Repeat\
    1.80 - \    (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
    1.81 + \    (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
    1.82   \      (Rewrite_Set SqRoot_simplify False))) e_\
    1.83   \ in [e_::bool])"
    1.84  ;