1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Wed Mar 07 14:20:33 2018 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Thu Mar 08 07:28:17 2018 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4  val bdv = [];
     1.5  val r = (((inst_bdv bdv) o norm o #prop o Thm.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 @@ -205,7 +205,7 @@
    1.13  "----- step 1: args for rew_";
    1.14  val ((t', asm'), (rules as r::rs), t) = ((e_term, []), equs, t);
    1.15  "----- step 2: rew_sub";
    1.16 -rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t;
    1.17 +rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;
    1.18  "----- step 3: step through rew_sub -- inefficient: goes into subterms";
    1.19  
    1.20  
    1.21 @@ -603,22 +603,22 @@
    1.22    Const ("HOL.eq", _) $ (Const ("Atools.pow", _) $ Var (("r", 0), _) $ Free ("2", _)) $
    1.23        (Const ("Groups.times_class.times", _) $ Var (("r", 0), _) $ Var (("r", 0), _)) => ()
    1.24  | _ => error "parse_patt  ?r ^^^ 2 = ?r * ?r  changed";
    1.25 -case parse thy str of
    1.26 +case parse thy term_str of
    1.27    NONE => ()
    1.28  | _ => writeln "parse does NOT take patterns with '?'";
    1.29  
    1.30  val t1 = (#prop o Thm.rep_thm) (num_str thm);
    1.31  if term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
    1.32  
    1.33 -val t2 = Trueprop $ (((parse_patt thy)) patt_str) : term;
    1.34 +val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term;
    1.35  if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
    1.36  
    1.37  (mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
    1.38  (*and   this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r"  [.]: thm
    1.39    gives a strange thm*);
    1.40 -(*while this*) 
    1.41 +(*while this..*) 
    1.42  val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r"  [.]: thm
    1.43 -  gives another strange thm; but it is used and words with rewriting: *);
    1.44 +  ..gives another strange thm; but it is used and works with rewriting: *);
    1.45  
    1.46  val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
    1.47  if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
    1.48 @@ -635,7 +635,7 @@
    1.49          (Const ("HOL.Trueprop", _) $
    1.50            (Const ("HOL.eq", _) $ _ $ _ )) => ()
    1.51  | _ => error "parse_patt  ?k \<noteq> 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n  changed";
    1.52 -case parse thy str of
    1.53 +case parse thy term_str of
    1.54    NONE => ()
    1.55  | _ => writeln "parse does NOT take patterns with '?'";
    1.56