1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Thu Mar 10 15:19:26 2011 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Thu Mar 10 16:04:00 2011 +0100
     1.3 @@ -37,7 +37,6 @@
     1.4  val bdv = [];
     1.5  val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm);
     1.6  "----- from old: and rew_sub";
     1.7 -(*========== inhibit exn =======================================================
     1.8  val (lhs,rhs) = (dest_equals' o strip_trueprop 
     1.9     	      o Logic.strip_imp_concl) r;
    1.10  (* old
    1.11 @@ -75,7 +74,6 @@
    1.12  Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r');
    1.13  Pretty.writeln (ProofContext.pretty_term_abbrev @{context} t');
    1.14  (*}*)
    1.15 -============ inhibit exn =====================================================*)
    1.16  
    1.17  "----------- test rewriting without Isac's thys ---------";
    1.18  "----------- test rewriting without Isac's thys ---------";
    1.19 @@ -86,7 +84,6 @@
    1.20  val ctxt = @{context};
    1.21  val thm =  @{thm add_commute};
    1.22  val tm = @{term "x + y*z::real"};
    1.23 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.24  
    1.25  val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
    1.26    handle _ => error "rewrite.sml diff.behav. in rewriting";
    1.27 @@ -114,7 +111,6 @@
    1.28  val tm = @{term "x*y + z::real"};
    1.29  val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)
    1.30    handle _ => error "rewrite.sml diff.behav. in rewriting";
    1.31 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    1.32  
    1.33  
    1.34  "----------- conditional rewriting without Isac's thys --";
    1.35 @@ -184,7 +180,7 @@
    1.36       val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) 
    1.37                                               (Logic.count_prems r', [], r'));
    1.38  case p' of
    1.39 -    [Const ("Not", _) $ (Const ("HOL.eq", _) $ Free ("y", _) $
    1.40 +    [Const ("HOL.Not", _) $ (Const ("HOL.eq", _) $ Free ("y", _) $
    1.41                                 Const ("Groups.zero_class.zero", _))] => ()
    1.42    | _ => error "rewrite.sml assumption changed";
    1.43  "=====^^^ make asms without Trueprop ---^^^";
    1.44 @@ -198,7 +194,7 @@
    1.45  "----------- step through 'fun rewrite_terms_'  ---------";
    1.46  "----- step 0: args for rewrite_terms_, local fun";
    1.47  val (thy, ord, erls, equs, t) =
    1.48 -    (theory "Biegelinie", dummy_ord, Erls, [str2term "x = 0"],
    1.49 +    (@{theory "Biegelinie"}, dummy_ord, Erls, [str2term "x = 0"],
    1.50       str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
    1.51  "----- step 1: args for rew_";
    1.52  val ((t', asm'), (rules as r::rs), t) = ((e_term, []), equs, t);
    1.53 @@ -298,7 +294,7 @@
    1.54  ----- 2009 -------------------------------------------------------------------*)
    1.55  
    1.56  (*the situation as was before repair (asm without Trueprop) is outcommented*)
    1.57 -val thy = theory "Isac";
    1.58 +val thy = @{theory "Isac"};
    1.59  "===== example which raised the problem =================";
    1.60  val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
    1.61  "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
    1.62 @@ -343,7 +339,6 @@
    1.63  trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
    1.64  "--------------------------------------------------------";
    1.65  
    1.66 -
    1.67  "----------- compare all prepat's existing 2010 ---------";
    1.68  "----------- compare all prepat's existing 2010 ---------";
    1.69  "----------- compare all prepat's existing 2010 ---------";
    1.70 @@ -375,7 +370,7 @@
    1.71    |> writeln
    1.72  *}
    1.73  end *)
    1.74 -val thy = theory "Isac";
    1.75 +val thy = @{theory "Isac"};
    1.76  val t = @{term "a + b * x = (0 ::real)"};
    1.77  val pat = parse_patt thy "?l = (?r ::real)";
    1.78  val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
    1.79 @@ -441,14 +436,18 @@
    1.80  "----------- fun app_rev, Rrls, -------------------------";
    1.81  "----------- fun app_rev, Rrls, -------------------------";
    1.82  val t = str2term "x^^^2 * x";
    1.83 +
    1.84  if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
    1.85  val tm = str2term "(x^^^2 * x) is_multUnordered";
    1.86 +eval_is_multUnordered "testid" "" tm thy;
    1.87 +
    1.88 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.89  case eval_is_multUnordered "testid" "" tm thy of
    1.90      SOME (_, Const ("HOL.Trueprop", _) $ 
    1.91                     (Const ("HOL.eq", _) $
    1.92                            (Const ("Poly.is'_multUnordered", _) $ _) $ 
    1.93 -                          Const ("True", _))) => ()
    1.94 -  | _ => error "rewrite.sml diff. eval_is_multUnordered 2";
    1.95 +                          Const ("HOL.True", _))) => ()
    1.96 +  | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
    1.97  
    1.98  tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := true;
    1.99  val SOME (t', _) = rewrite_set_ thy true order_mult_ t;