1.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Mon Dec 07 10:17:08 2015 +0100
     1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Mon Dec 07 10:52:07 2015 +0100
     1.3 @@ -34,14 +34,14 @@
     1.4          val (deriv, {thy = thy, tags = tags, maxidx = maxidx, 
     1.5                       shyps = shyps, hyps = hyps, tpairs = tpairs, 
     1.6                       prop = prop}) = 
     1.7 -	    rep_thm_G thm;
     1.8 +	    Thm.rep_thm_G thm;
     1.9          val (lhs,rhs) = (dest_equals' o strip_trueprop 
    1.10  		         o Logic.strip_imp_concl) prop;
    1.11          val prop' = case strip_imp_prems' prop of
    1.12  		        NONE => Trueprop $ (mk_equality (rhs, lhs))
    1.13  		      | SOME cs => 
    1.14  		        ins_concl cs (Trueprop $ (mk_equality (rhs, lhs)));
    1.15 -    in assbl_thm deriv thy tags maxidx shyps hyps tpairs prop' end;
    1.16 +    in Thm.assbl_thm deriv thy tags maxidx shyps hyps tpairs prop' end;
    1.17  (*
    1.18    (sym RS real_mult_div_cancel1) handle e => print_exn e;
    1.19  Exception THM 1 raised:

     2.1 --- a/src/Tools/isac/Interpret/script.sml	Mon Dec 07 10:17:08 2015 +0100
     2.2 +++ b/src/Tools/isac/Interpret/script.sml	Mon Dec 07 10:52:07 2015 +0100
     2.3 @@ -683,7 +683,7 @@
     2.4  
     2.5  fun make_rule thy t =
     2.6    let val ct = Thm.global_cterm_of thy (Trueprop $ t)
     2.7 -  in Thm (term_to_string''' thy (term_of ct), make_thm ct) end;
     2.8 +  in Thm (term_to_string''' thy (term_of ct), Thm.make_thm ct) end;
     2.9  
    2.10  (* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m;
    2.11     *)

     3.1 --- a/src/Tools/isac/ProgLang/calculate.sml	Mon Dec 07 10:17:08 2015 +0100
     3.2 +++ b/src/Tools/isac/ProgLang/calculate.sml	Mon Dec 07 10:52:07 2015 +0100
     3.3 @@ -192,7 +192,7 @@
     3.4      NONE => ((* tracing ("@@@ get_calculation: NONE, op_= " ^ op_);
     3.5        tracing ("@@@ get_calculation: ct= "); atomty ct; *)
     3.6        NONE)
     3.7 -  | SOME (thmid, t) => SOME (thmid, (make_thm o (Thm.global_cterm_of thy)) t);
     3.8 +  | SOME (thmid, t) => SOME (thmid, (Thm.make_thm o (Thm.global_cterm_of thy)) t);
     3.9  (*
    3.10  > val ct = (the o (parse thy)) "#9 is_const";
    3.11  > get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;
    3.12 @@ -307,7 +307,7 @@
    3.13      case eval_fn op_ ct thy of
    3.14  	NONE => NONE
    3.15        | SOME (thmid,t) =>
    3.16 -	SOME (thmid, (make_thm o (Thm.global_cterm_of thy)) t);
    3.17 +	SOME (thmid, (Thm.make_thm o (Thm.global_cterm_of thy)) t);
    3.18  
    3.19  
    3.20  

     4.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Mon Dec 07 10:17:08 2015 +0100
     4.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Mon Dec 07 10:52:07 2015 +0100
     4.3 @@ -317,13 +317,13 @@
     4.4  fun get_rls_scr rls' = ((#scr o rep_rls o assoc_rls) rls')
     4.5    handle _ => error ("get_rls_scr: no script for " ^ rls');
     4.6  
     4.7 -(*make_thm added to Pure/thm.ML*)
     4.8 +(*Thm.make_thm added to Pure/thm.ML*)
     4.9  fun mk_thm thy str = 
    4.10      let val t = (term_of o the o (parse thy)) str
    4.11  	val t' = case t of
    4.12  		     Const ("==>",_) $ _ $ _ => t
    4.13  		   | _ => Trueprop $ t
    4.14 -    in make_thm (Thm.global_cterm_of thy t') end;
    4.15 +    in Thm.make_thm (Thm.global_cterm_of thy t') end;
    4.16  (*
    4.17    val str = "?r ^^^ 2 = ?r * ?r";
    4.18    val thm = realpow_twoI;

     5.1 --- a/src/Tools/isac/ProgLang/termC.sml	Mon Dec 07 10:17:08 2015 +0100
     5.2 +++ b/src/Tools/isac/ProgLang/termC.sml	Mon Dec 07 10:52:07 2015 +0100
     5.3 @@ -733,15 +733,15 @@
     5.4    let 
     5.5      val {sign_ref = sign_ref, der = der, maxidx = maxidx,
     5.6  	    shyps = shyps, hyps = hyps, (*tpairs = tpairs,*) prop = prop} = 
     5.7 -	rep_thm_G thm;
     5.8 +	Thm.rep_thm_G thm;
     5.9      val prop' = app_num_tr'1 prop;
    5.10 -  in assbl_thm sign_ref der maxidx shyps hyps (*tpairs*) prop' end;*)
    5.11 +  in Thm.assbl_thm sign_ref der maxidx shyps hyps (*tpairs*) prop' end;*)
    5.12  fun num_str thm =
    5.13    let val (deriv, 
    5.14  	   {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps, 
    5.15 -	    hyps = hyps, tpairs = tpairs, prop = prop}) = rep_thm_G thm
    5.16 +	    hyps = hyps, tpairs = tpairs, prop = prop}) = Thm.rep_thm_G thm
    5.17      val prop' = numbers_to_string prop;
    5.18 -  in assbl_thm deriv thy tags maxidx shyps hyps tpairs prop' end;
    5.19 +  in Thm.assbl_thm deriv thy tags maxidx shyps hyps tpairs prop' end;
    5.20  
    5.21  fun get_thm' xstring = (*?covers 2009 Thm?!, replaces 2002 fun get_thm :
    5.22  val it = fn : theory -> xstring -> Thm.thm*)