1.1 --- a/test/Tools/isac/Interpret/script.sml	Thu Nov 21 17:31:20 2013 +0100
     1.2 +++ b/test/Tools/isac/Interpret/script.sml	Thu Nov 21 18:12:17 2013 +0100
     1.3 @@ -152,7 +152,7 @@
     1.4            ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
     1.5               [],
     1.6               [Const ("HOL.Trueprop", "bool => prop") $
     1.7 -                   (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
     1.8 +                   (Const ("HOL.eq", "["Real.real, bool] => bool") $ ... $ ...)])
     1.9         raised
    1.10      ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
    1.11      ie. the argument had not been simplified before          ^^^^^^^^^^^^^^^
    1.12 @@ -300,7 +300,7 @@
    1.13  val (pt, p) = case locatetac tac (pt,p) of
    1.14  	("ok", (_, _, ptp))  => ptp | _ => error "script.sml locatetac";
    1.15  "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
    1.16 -val pIopt = get_pblID (pt,ip); (*SOME ["linear", "univariate", "equation", "test"]*)
    1.17 +val pIopt = get_pblID (pt,ip); (*SOME ["LINEAR", "univariate", "equation", "test"]*)
    1.18  tacis; (*= []*)
    1.19  member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
    1.20  "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
    1.21 @@ -313,7 +313,7 @@
    1.22  val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
    1.23  "~~~~~ dont like to go into nstep_up...";
    1.24  val t = str2term ("SubProblem" ^ 
    1.25 -  "(Test', [linear, univariate, equation, test], [Test, solve_linear])" ^
    1.26 +  "(Test', [LINEAR, univariate, equation, test], [Test, solve_linear])" ^
    1.27    "[BOOL (-1 + x = 0), REAL x]");
    1.28  val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)
    1.29  case tac_ of 
    1.30 @@ -419,7 +419,7 @@
    1.31  
    1.32  val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
    1.33  val (p'''', pt'''') = (p, pt);
    1.34 -f2str f = "-1 + x = 0"; snd nxt = Subproblem ("Test", ["linear", "univariate", "equation", "test"]);
    1.35 +f2str f = "-1 + x = 0"; snd nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]);
    1.36  val (p, p_) = p(* = ([2], Res)*);
    1.37  val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
    1.38  val (env, loc_, curry_arg, res, Safe, false) = scrstate;
    1.39 @@ -493,7 +493,7 @@
    1.40  
    1.41   val tacs = sel_rules pt ([1],Res);
    1.42   if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
    1.43 -      Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
    1.44 +      Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
    1.45        Check_elementwise "Assumptions"] then ()
    1.46   else error "script.sml: diff.behav. in sel_rules ([1],Res)";
    1.47  
    1.48 @@ -508,7 +508,7 @@
    1.49  
    1.50   val tacs = sel_rules pt ([3],Res);
    1.51   if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
    1.52 -      Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
    1.53 +      Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
    1.54        Check_elementwise "Assumptions"] then ()
    1.55   else error "script.sml: diff.behav. in sel_rules ([3],Res)";
    1.56  
    1.57 @@ -535,14 +535,14 @@
    1.58  val ((pt, _), _) = get_calc cI;
    1.59  (*version 1:*)
    1.60  if sel_rules pt p = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
    1.61 -  Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
    1.62 +  Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
    1.63    Check_elementwise "Assumptions"] then ()
    1.64  else error "fetchApplicableTactics ([1],Res) changed";
    1.65  (*version 2:*)
    1.66  (*WAS:
    1.67  sel_appl_atomic_tacs pt p;
    1.68  ...
    1.69 -### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["linear","univariate","equation","test"])' 
    1.70 +### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])' 
    1.71  ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"' 
    1.72  *)
    1.73  
    1.74 @@ -568,7 +568,7 @@
    1.75  (*WN120611 stopped and took version 1 again for fetchApplicableTactics !
    1.76  (distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs
    1.77  ...
    1.78 -### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["linear","univariate","equation","test"])' 
    1.79 +### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])' 
    1.80  ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"' 
    1.81  *)
    1.82