1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Sat Mar 19 15:09:19 2011 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Sat Mar 19 15:18:10 2011 +0100
     1.3 @@ -37,23 +37,23 @@
     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 -val (lhs,rhs) = (dest_equals' o strip_trueprop 
     1.8 +val (LHS,RHS) = (dest_equals' o strip_trueprop 
     1.9     	      o Logic.strip_imp_concl) r;
    1.10  (* old
    1.11 -val insts = Pattern.match thy (lhs,t) (Vartab.empty, Vartab.empty);*)
    1.12 +val insts = Pattern.match thy (LHS,t) (Vartab.empty, Vartab.empty);*)
    1.13  "----- fun match_rew in Pure/pattern.ML";
    1.14 -val rtm = the_default rhs (Term.rename_abs lhs t rhs);
    1.15 +val rtm = the_default RHS (Term.rename_abs LHS t RHS);
    1.16  
    1.17  writeln(Syntax.string_of_term ctxt rtm);
    1.18 -writeln(Syntax.string_of_term ctxt lhs);
    1.19 +writeln(Syntax.string_of_term ctxt LHS);
    1.20  writeln(Syntax.string_of_term ctxt t);
    1.21  
    1.22 -(Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty));
    1.23 -val (rew, rhs) = (Envir.subst_term 
    1.24 -  (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
    1.25 +(Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
    1.26 +val (rew, RHS) = (Envir.subst_term 
    1.27 +  (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
    1.28  (*lookup in isabelle?trace?response...*)
    1.29  writeln(Syntax.string_of_term ctxt rew);
    1.30 -writeln(Syntax.string_of_term ctxt rhs);
    1.31 +writeln(Syntax.string_of_term ctxt RHS);
    1.32  
    1.33  "===== rewriting: prep insertion into rew_sub";
    1.34  val thy = @{theory Complex_Main};
    1.35 @@ -62,9 +62,9 @@
    1.36  val r = Thm.prop_of thm;
    1.37  val tm = @{term "x*2 / 2::real"};
    1.38  "----- and rew_sub";
    1.39 -val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
    1.40 +val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
    1.41                    o Logic.strip_imp_concl) r;
    1.42 -val r' = Envir.subst_term (Pattern.match thy (lhs, tm) 
    1.43 +val r' = Envir.subst_term (Pattern.match thy (LHS, tm) 
    1.44                                  (Vartab.empty, Vartab.empty)) r;
    1.45  val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
    1.46  val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 
    1.47 @@ -129,14 +129,14 @@
    1.48  val prems = Logic.strip_prems (nps, [], rule);
    1.49  
    1.50  val eq = Logic.strip_imp_concl rule;
    1.51 -val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
    1.52 +val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
    1.53  
    1.54 -val mtcs = Pattern.match thy (lhs, tm) (Vartab.empty, Vartab.empty);
    1.55 +val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
    1.56  val rule' = Envir.subst_term mtcs rule;
    1.57  
    1.58  val prems' = (fst o Logic.strip_prems) 
    1.59                (Logic.count_prems rule', [], rule');
    1.60 -val rhs' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 
    1.61 +val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 
    1.62              o Logic.strip_imp_concl) rule';
    1.63  
    1.64  "----- conditional rewriting creating an assumption";
    1.65 @@ -164,14 +164,14 @@
    1.66  "----- evaluate arguments";
    1.67  val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = 
    1.68      (thy, 0, [], dummy_ord, e_rls, true, [], (prop_of thm), tm);
    1.69 -"----- step 1: lhs, rhs of rule";
    1.70 -     val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
    1.71 +"----- step 1: LHS, RHS of rule";
    1.72 +     val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
    1.73                         o Logic.strip_imp_concl) r;
    1.74  term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a";
    1.75 -term2str lhs = "?a * ?b / ?b"; term2str rhs = "?a";
    1.76 +term2str LHS = "?a * ?b / ?b"; term2str RHS = "?a";
    1.77  "----- step 2: the rule instantiated";
    1.78       val r' = Envir.subst_term 
    1.79 -                  (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r;
    1.80 +                  (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
    1.81  term2str r' = "y ~= 0 ==> x * y / y = x";
    1.82  "----- step 3: get the (instantiated) assumption(s)";
    1.83       val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
    1.84 @@ -184,7 +184,7 @@
    1.85                                 Const ("Groups.zero_class.zero", _))] => ()
    1.86    | _ => error "rewrite.sml assumption changed";
    1.87  "=====^^^ make asms without Trueprop ---^^^";
    1.88 -"----- step 4: get the (instantiated) rhs";
    1.89 +"----- step 4: get the (instantiated) RHS";
    1.90       val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 
    1.91                 o Logic.strip_imp_concl) r';
    1.92  term2str t' = "x";