diff -r 4eaee5e76e23 -r 911c49949ba9 test/Tools/isac/Knowledge/algein.sml
--- a/test/Tools/isac/Knowledge/algein.sml	Thu Jul 21 12:01:56 2011 +0200
+++ b/test/Tools/isac/Knowledge/algein.sml	Fri Jul 22 14:01:09 2011 +0200
@@ -17,8 +17,7 @@
 "-----------------------------------------------------------------";
 "-----------------------------------------------------------------";
 
-(*=== inhibit exn ?=============================================================
-val thy = AlgEin.thy;
+val thy = @{theory "AlgEin"};
 
 
 (* use"../smltest/IsacKnowledge/algein.sml";
@@ -33,8 +32,10 @@
 \ (let t_ = (l_ = 1)\
 \ in t_)"
 ;
+(*=== inhibit exn 110722=============================================================
 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
-(*---^^^-OK-----------------------------------------------------------------*)
+=== inhibit exn 110722=============================================================*)
+
 val str =
 "Script RechnenSymbolScript (k_::bool) (q__::bool)           \
 \(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
@@ -46,14 +47,12 @@
 \      t_ = Repeat (Try (Rewrite_Set norm_Poly False)) t_\
 \ in t_)"
 ;
+(*=== inhibit exn 110722=============================================================
 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
-(*---vvv-NOTok--------------------------------------------------------------*)
-
-
 
 atomty sc;
 atomt sc;
-
+=== inhibit exn 110722=============================================================*)
 
 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
@@ -68,6 +67,7 @@
   ("Isac",["numerischSymbolische", "Berechnung"],
    ["Berechnung","erstNumerisch"]);
 val p = e_pos'; val c = [];
+(*=== inhibit exn 110722=============================================================
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*);
 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenLaenge (k = 10)"*);
 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "Querschnitt (q = 1)"*);
@@ -97,12 +97,12 @@
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then ()
 else error "algein.sml diff.behav. in erstSymbolisch 99";
-
+ DEconstrCalcTree 1;
+=== inhibit exn 110722=============================================================*)
 
 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
-states:=[];
 CalcTree
 [(["KantenLaenge (k=10)","Querschnitt (q=1)",
    "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]", 
@@ -115,9 +115,10 @@
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
 val ((pt,p),_) = get_calc 1; show_pt pt;
+(*=== inhibit exn 110722=============================================================
 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()
 else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
-
+===== inhibit exn 110722===========================================================*)
 (*
 show_pt pt;
 trace_rewrite:=true;
@@ -125,14 +126,13 @@
 trace_script:=true;
 trace_script:=false;
 *)
-
 "----------- Widerspruch 3 = 777 ---------------------------------";
 "----------- Widerspruch 3 = 777 ---------------------------------";
 "----------- Widerspruch 3 = 777 ---------------------------------";
-val thy = (theory "Isac"); 
+val thy = @{theory "Isac"}; 
 val rew_ord = dummy_ord;
 val erls = Erls;
-
+(*===== inhibit exn 110722===========================================================
 val thm = assoc_thm' thy ("sym_real_mult_0_right","");
 val t = str2term "0 = 0";
 val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
@@ -148,6 +148,7 @@
 val t'' = subst_atomic subst t';
 term2str t'';
 (********"0 = 3 * 0"*)
+===== inhibit exn 110722===========================================================*)
 
 val thm = assoc_thm' thy ("sym","");
 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
@@ -157,4 +158,3 @@
 (* use"../smltest/IsacKnowledge/algein.sml";
    *)
 
-===== inhibit exn ?===========================================================*)