1.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Mon Dec 07 11:25:02 2015 +0100
     1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Mon Dec 07 11:32:12 2015 +0100
     1.3 @@ -449,7 +449,7 @@
     1.4  	         let
     1.5               val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
     1.6               val thm_deriv = Thm.get_name_hint thm
     1.7 -             val thminst = inst_bdv subst ((norm o #prop o rep_thm) thm)
     1.8 +             val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)
     1.9  	         in
    1.10  	           ContThmInst
    1.11  	            {thyID   = theory'2thyID thy',
    1.12 @@ -474,7 +474,7 @@
    1.13               val pp = par_pblobj pt p
    1.14               val thy' = get_obj g_domID pt pp
    1.15               val subst = subs2subst (assoc_thy thy') subs
    1.16 -             val thminst = inst_bdv subst ((norm o #prop o rep_thm) thm)
    1.17 +             val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)
    1.18               val f = case p_ of
    1.19                   Frm => get_obj g_form pt p
    1.20                 | Res => (fst o (get_obj g_result pt)) p

     2.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Mon Dec 07 11:25:02 2015 +0100
     2.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Mon Dec 07 11:32:12 2015 +0100
     2.3 @@ -53,7 +53,7 @@
     2.4    (let
     2.5      val (t',asms,lrd,rew) = 
     2.6  	rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
     2.7 -		(((inst_bdv bdv) o norm o #prop o rep_thm) thm) ct;
     2.8 +		(((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm) ct;
     2.9    in if rew then SOME (t', distinct asms)
    2.10       else NONE end)
    2.11  (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)

     3.1 --- a/src/Tools/isac/ProgLang/scrtools.sml	Mon Dec 07 11:25:02 2015 +0100
     3.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml	Mon Dec 07 11:32:12 2015 +0100
     3.3 @@ -430,7 +430,7 @@
     3.4   atomt tt; tracing (term2str tt);
     3.5   *)
     3.6  
     3.7 -val contains_bdv = (not o null o (filter is_bdv) o ids2str o #prop o rep_thm);
     3.8 +val contains_bdv = (not o null o (filter is_bdv) o ids2str o #prop o Thm.rep_thm);
     3.9  
    3.10  (*.does a rule contain a 'bdv'; descend recursively into Rls_.*)
    3.11  fun contain_bdv [] = false

     4.1 --- a/src/Tools/isac/ProgLang/termC.sml	Mon Dec 07 11:25:02 2015 +0100
     4.2 +++ b/src/Tools/isac/ProgLang/termC.sml	Mon Dec 07 11:32:12 2015 +0100
     4.3 @@ -1119,7 +1119,7 @@
     4.4  let fun mk_sub ((id, _), (ty, tm)) = (Free (id, ty), tm) in
     4.5  map mk_sub subs end;
     4.6  
     4.7 -val atomthm = atomt o #prop o rep_thm;
     4.8 +val atomthm = atomt o #prop o Thm.rep_thm;
     4.9  
    4.10  (*.instantiate #prop thm with bound variables (as Free).*)
    4.11  fun inst_bdv [] t = t : term