1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Fri Mar 04 11:45:02 2011 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Thu Mar 10 12:45:58 2011 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4  "----------- assemble rewrite ---------------------------";
     1.5  "----------- assemble rewrite ---------------------------";
     1.6  "===== rewriting by thm with 'a";
     1.7 -show_types := true;
     1.8 +(*show_types := true;*)
     1.9  val thy = @{theory Complex_Main};
    1.10  val ctxt = @{context};
    1.11  val thm = @{thm add_commute};
    1.12 @@ -37,6 +37,7 @@
    1.13  val bdv = [];
    1.14  val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm);
    1.15  "----- from old: and rew_sub";
    1.16 +(*========== inhibit exn =======================================================
    1.17  val (lhs,rhs) = (dest_equals' o strip_trueprop 
    1.18     	      o Logic.strip_imp_concl) r;
    1.19  (* old
    1.20 @@ -74,6 +75,7 @@
    1.21  Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r');
    1.22  Pretty.writeln (ProofContext.pretty_term_abbrev @{context} t');
    1.23  (*}*)
    1.24 +============ inhibit exn =====================================================*)
    1.25  
    1.26  "----------- test rewriting without Isac's thys ---------";
    1.27  "----------- test rewriting without Isac's thys ---------";
    1.28 @@ -84,6 +86,7 @@
    1.29  val ctxt = @{context};
    1.30  val thm =  @{thm add_commute};
    1.31  val tm = @{term "x + y*z::real"};
    1.32 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.33  
    1.34  val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
    1.35    handle _ => error "rewrite.sml diff.behav. in rewriting";
    1.36 @@ -111,6 +114,7 @@
    1.37  val tm = @{term "x*y + z::real"};
    1.38  val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)
    1.39    handle _ => error "rewrite.sml diff.behav. in rewriting";
    1.40 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    1.41  
    1.42  
    1.43  "----------- conditional rewriting without Isac's thys --";
    1.44 @@ -160,7 +164,7 @@
    1.45  (*and make asms without Trueprop, beginning with the result:*)
    1.46  val tm = @{term "x*y / y::real"};
    1.47  val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (prop_of thm) tm;
    1.48 -show_types := false;
    1.49 +(*show_types := false;*)
    1.50  "----- evaluate arguments";
    1.51  val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = 
    1.52      (thy, 0, [], dummy_ord, e_rls, true, [], (prop_of thm), tm);
    1.53 @@ -325,7 +329,7 @@
    1.54  (*checked visually: trace_rewrite looks like above for 2009*)
    1.55  
    1.56  trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
    1.57 -show_types := false;
    1.58 +(*show_types := false;*)
    1.59  writeln "----- rewrite_ rat_mult_poly_r--------------------------";
    1.60  val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
    1.61  (*t' = t''; (*false because of further rewrites in t'*)*)
    1.62 @@ -440,7 +444,7 @@
    1.63  if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
    1.64  val tm = str2term "(x^^^2 * x) is_multUnordered";
    1.65  case eval_is_multUnordered "testid" "" tm thy of
    1.66 -    SOME (_, Const ("Trueprop", _) $ 
    1.67 +    SOME (_, Const ("HOL.Trueprop", _) $ 
    1.68                     (Const ("HOL.eq", _) $
    1.69                            (Const ("Poly.is'_multUnordered", _) $ _) $ 
    1.70                            Const ("True", _))) => ()
    1.71 @@ -522,5 +526,4 @@
    1.72      ([], true) => ()
    1.73    | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
    1.74  
    1.75 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.76  -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)