test/Tools/isac/Interpret/script.sml
changeset 42387 767debe8a50c
parent 42283 b95f0dde56c1
child 42394 977788dfed26
     1.1 --- a/test/Tools/isac/Interpret/script.sml	Thu Mar 08 14:33:34 2012 +0100
     1.2 +++ b/test/Tools/isac/Interpret/script.sml	Sat Mar 10 09:41:09 2012 +0100
     1.3 @@ -135,10 +135,9 @@
     1.4  val (p,_,f,nxt,_,pt) = me nxt p c pt;
     1.5  case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
     1.6  	  | _ => error "script.sml, doesnt find Substitute #2";
     1.7 -
     1.8 -(*========== inhibit exn AK110721 ================================================
     1.9  (* ERROR: caused by f2str f *)
    1.10  trace_rewrite:=true;
    1.11 +
    1.12  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
    1.13  trace_rewrite:=false;
    1.14    (*Exception TYPE raised:
    1.15 @@ -155,22 +154,12 @@
    1.16      ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
    1.17      ie. the argument had not been simplified before          ^^^^^^^^^^^^^^^
    1.18      thus corrected eval_argument_in OK*)
    1.19 -========== inhibit exn AK110721 ================================================*)
    1.20 -
    1.21  val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
    1.22 -val e1__e1 = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";
    1.23 +val e1__e1 = str2term "NTH 1 [M_b 0 = 0, M_b L = 0]";
    1.24  val e1__e1 = eval_listexpr_ @{theory Biegelinie} srls e1__e1; term2str e1__e1;
    1.25 -
    1.26 -(*========== inhibit exn 110721 ================================================
    1.27 -(*AK110722
    1.28 - TRIAL: Should be the same
    1.29 - term2str e1__e1 = "M_b 0 = 0";
    1.30 - term2str e1__e1;*)
    1.31 -
    1.32  if term2str e1__e1 = "M_b 0 = 0"
    1.33    then ()
    1.34    else error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
    1.35 -========== inhibit exn 110721 ================================================*)
    1.36  
    1.37  (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
    1.38   val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
    1.39 @@ -180,16 +169,13 @@
    1.40   val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
    1.41  
    1.42  val l__l = str2term "lhs (M_b 0 = 0)";
    1.43 -(*AK110722 eval_listexpr_ is prob. without _ ????*)
    1.44  val l__l = eval_listexpr_ @{theory Biegelinie} srls l__l; term2str l__l;
    1.45  val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
    1.46 -(*========== inhibit exn 110721 ================================================
    1.47 -trace_rewrite:=true;
    1.48 +
    1.49  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
    1.50 -trace_rewrite:=false;
    1.51 -========== inhibit exn 110721 ================================================*)
    1.52 +if nxt = ("Rewrite", Rewrite ("Belastung_Querkraft", "Biegelinie.Belastung_Querkraft"))
    1.53 +then () else error "";
    1.54  
    1.55 -show_mets();
    1.56  
    1.57  "----------- fun sel_appl_atomic_tacs ----------------------------";
    1.58  "----------- fun sel_appl_atomic_tacs ----------------------------";