1.1 --- a/test/Tools/isac/Interpret/mstools.sml	Sat Mar 19 15:09:19 2011 +0100
     1.2 +++ b/test/Tools/isac/Interpret/mstools.sml	Sat Mar 19 15:18:10 2011 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4  val ctxt = ProofContext.init_global @{theory}
     1.5        |> declare_constraints "xxx + yyy = (111::int)";
     1.6  val t = parseNEW ctxt "xxx = 123";
     1.7 -if ((rhs t) |> type_of) = @{typ int} then ()
     1.8 +if ((lhs t) |> type_of) = @{typ int} then ()
     1.9    else error "mstools: incorrect type inference from parseNEW ctxt";
    1.10  
    1.11  (*========== inhibit exn =======================================================

     2.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Sat Mar 19 15:09:19 2011 +0100
     2.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Sat Mar 19 15:18:10 2011 +0100
     2.3 @@ -37,23 +37,23 @@
     2.4  val bdv = [];
     2.5  val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm);
     2.6  "----- from old: and rew_sub";
     2.7 -val (lhs,rhs) = (dest_equals' o strip_trueprop 
     2.8 +val (LHS,RHS) = (dest_equals' o strip_trueprop 
     2.9     	      o Logic.strip_imp_concl) r;
    2.10  (* old
    2.11 -val insts = Pattern.match thy (lhs,t) (Vartab.empty, Vartab.empty);*)
    2.12 +val insts = Pattern.match thy (LHS,t) (Vartab.empty, Vartab.empty);*)
    2.13  "----- fun match_rew in Pure/pattern.ML";
    2.14 -val rtm = the_default rhs (Term.rename_abs lhs t rhs);
    2.15 +val rtm = the_default RHS (Term.rename_abs LHS t RHS);
    2.16  
    2.17  writeln(Syntax.string_of_term ctxt rtm);
    2.18 -writeln(Syntax.string_of_term ctxt lhs);
    2.19 +writeln(Syntax.string_of_term ctxt LHS);
    2.20  writeln(Syntax.string_of_term ctxt t);
    2.21  
    2.22 -(Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty));
    2.23 -val (rew, rhs) = (Envir.subst_term 
    2.24 -  (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
    2.25 +(Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
    2.26 +val (rew, RHS) = (Envir.subst_term 
    2.27 +  (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
    2.28  (*lookup in isabelle?trace?response...*)
    2.29  writeln(Syntax.string_of_term ctxt rew);
    2.30 -writeln(Syntax.string_of_term ctxt rhs);
    2.31 +writeln(Syntax.string_of_term ctxt RHS);
    2.32  
    2.33  "===== rewriting: prep insertion into rew_sub";
    2.34  val thy = @{theory Complex_Main};
    2.35 @@ -62,9 +62,9 @@
    2.36  val r = Thm.prop_of thm;
    2.37  val tm = @{term "x*2 / 2::real"};
    2.38  "----- and rew_sub";
    2.39 -val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
    2.40 +val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
    2.41                    o Logic.strip_imp_concl) r;
    2.42 -val r' = Envir.subst_term (Pattern.match thy (lhs, tm) 
    2.43 +val r' = Envir.subst_term (Pattern.match thy (LHS, tm) 
    2.44                                  (Vartab.empty, Vartab.empty)) r;
    2.45  val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
    2.46  val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 
    2.47 @@ -129,14 +129,14 @@
    2.48  val prems = Logic.strip_prems (nps, [], rule);
    2.49  
    2.50  val eq = Logic.strip_imp_concl rule;
    2.51 -val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
    2.52 +val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
    2.53  
    2.54 -val mtcs = Pattern.match thy (lhs, tm) (Vartab.empty, Vartab.empty);
    2.55 +val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
    2.56  val rule' = Envir.subst_term mtcs rule;
    2.57  
    2.58  val prems' = (fst o Logic.strip_prems) 
    2.59                (Logic.count_prems rule', [], rule');
    2.60 -val rhs' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 
    2.61 +val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 
    2.62              o Logic.strip_imp_concl) rule';
    2.63  
    2.64  "----- conditional rewriting creating an assumption";
    2.65 @@ -164,14 +164,14 @@
    2.66  "----- evaluate arguments";
    2.67  val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = 
    2.68      (thy, 0, [], dummy_ord, e_rls, true, [], (prop_of thm), tm);
    2.69 -"----- step 1: lhs, rhs of rule";
    2.70 -     val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
    2.71 +"----- step 1: LHS, RHS of rule";
    2.72 +     val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
    2.73                         o Logic.strip_imp_concl) r;
    2.74  term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a";
    2.75 -term2str lhs = "?a * ?b / ?b"; term2str rhs = "?a";
    2.76 +term2str LHS = "?a * ?b / ?b"; term2str RHS = "?a";
    2.77  "----- step 2: the rule instantiated";
    2.78       val r' = Envir.subst_term 
    2.79 -                  (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r;
    2.80 +                  (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
    2.81  term2str r' = "y ~= 0 ==> x * y / y = x";
    2.82  "----- step 3: get the (instantiated) assumption(s)";
    2.83       val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
    2.84 @@ -184,7 +184,7 @@
    2.85                                 Const ("Groups.zero_class.zero", _))] => ()
    2.86    | _ => error "rewrite.sml assumption changed";
    2.87  "=====^^^ make asms without Trueprop ---^^^";
    2.88 -"----- step 4: get the (instantiated) rhs";
    2.89 +"----- step 4: get the (instantiated) RHS";
    2.90       val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 
    2.91                 o Logic.strip_imp_concl) r';
    2.92  term2str t' = "x";