1.1 --- a/src/Tools/isac/Frontend/Frontend.thy	Thu Nov 21 09:18:22 2013 +0100
     1.2 +++ b/src/Tools/isac/Frontend/Frontend.thy	Thu Nov 21 11:17:42 2013 +0100
     1.3 @@ -16,5 +16,5 @@
     1.4    ML_file "~~/src/Tools/isac/Frontend/states.sml"
     1.5    ML_file "~~/src/Tools/isac/Frontend/interface.sml"
     1.6  
     1.7 -  use "~~/src/Tools/isac/print_exn_G.sml"
     1.8 +  ML_file "~~/src/Tools/isac/print_exn_G.sml"
     1.9  end
    1.10 \ No newline at end of file

     2.1 --- a/src/Tools/isac/Interpret/Interpret.thy	Thu Nov 21 09:18:22 2013 +0100
     2.2 +++ b/src/Tools/isac/Interpret/Interpret.thy	Thu Nov 21 11:17:42 2013 +0100
     2.3 @@ -5,28 +5,16 @@
     2.4  
     2.5  theory Interpret
     2.6  imports "~~/src/Tools/isac/ProgLang/ProgLang"
     2.7 -uses 
     2.8 -  ("~~/src/Tools/isac/Interpret/mstools.sml") 
     2.9 -  ("~~/src/Tools/isac/Interpret/ctree.sml") 
    2.10 -  ("~~/src/Tools/isac/Interpret/ptyps.sml") 
    2.11 -  ("~~/src/Tools/isac/Interpret/generate.sml")
    2.12 -  ("~~/src/Tools/isac/Interpret/calchead.sml") 
    2.13 -  ("~~/src/Tools/isac/Interpret/appl.sml") 
    2.14 -  ("~~/src/Tools/isac/Interpret/rewtools.sml") 
    2.15 -  ("~~/src/Tools/isac/Interpret/script.sml")
    2.16 -  ("~~/src/Tools/isac/Interpret/solve.sml") 
    2.17 -  ("~~/src/Tools/isac/Interpret/inform.sml") 
    2.18 -  ("~~/src/Tools/isac/Interpret/mathengine.sml")
    2.19  begin
    2.20 -  use "~~/src/Tools/isac/Interpret/mstools.sml"
    2.21 -  use "~~/src/Tools/isac/Interpret/ctree.sml"
    2.22 -  use "~~/src/Tools/isac/Interpret/ptyps.sml"
    2.23 -  use "~~/src/Tools/isac/Interpret/generate.sml"
    2.24 -  use "~~/src/Tools/isac/Interpret/calchead.sml"
    2.25 -  use "~~/src/Tools/isac/Interpret/appl.sml"
    2.26 -  use "~~/src/Tools/isac/Interpret/rewtools.sml"
    2.27 -  use "~~/src/Tools/isac/Interpret/script.sml"
    2.28 -  use "~~/src/Tools/isac/Interpret/solve.sml"
    2.29 -  use "~~/src/Tools/isac/Interpret/inform.sml"
    2.30 -  use "~~/src/Tools/isac/Interpret/mathengine.sml"
    2.31 +  ML_file "~~/src/Tools/isac/Interpret/mstools.sml"
    2.32 +  ML_file "~~/src/Tools/isac/Interpret/ctree.sml"
    2.33 +  ML_file "~~/src/Tools/isac/Interpret/ptyps.sml"
    2.34 +  ML_file "~~/src/Tools/isac/Interpret/generate.sml"
    2.35 +  ML_file "~~/src/Tools/isac/Interpret/calchead.sml"
    2.36 +  ML_file "~~/src/Tools/isac/Interpret/appl.sml"
    2.37 +  ML_file "~~/src/Tools/isac/Interpret/rewtools.sml"
    2.38 +  ML_file "~~/src/Tools/isac/Interpret/script.sml"
    2.39 +  ML_file "~~/src/Tools/isac/Interpret/solve.sml"
    2.40 +  ML_file "~~/src/Tools/isac/Interpret/inform.sml"
    2.41 +  ML_file "~~/src/Tools/isac/Interpret/mathengine.sml"
    2.42  end
    2.43 \ No newline at end of file

     3.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Thu Nov 21 09:18:22 2013 +0100
     3.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Thu Nov 21 11:17:42 2013 +0100
     3.3 @@ -31,7 +31,7 @@
     3.4  *)
     3.5  fun sym_thm thm =
     3.6      let 
     3.7 -        val (deriv, {thy_ref = thy_ref, tags = tags, maxidx = maxidx, 
     3.8 +        val (deriv, {thy = thy, tags = tags, maxidx = maxidx, 
     3.9                       shyps = shyps, hyps = hyps, tpairs = tpairs, 
    3.10                       prop = prop}) = 
    3.11  	    rep_thm_G thm;
    3.12 @@ -41,7 +41,7 @@
    3.13  		        NONE => Trueprop $ (mk_equality (rhs, lhs))
    3.14  		      | SOME cs => 
    3.15  		        ins_concl cs (Trueprop $ (mk_equality (rhs, lhs)));
    3.16 -    in assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop' end;
    3.17 +    in assbl_thm deriv thy tags maxidx shyps hyps tpairs prop' end;
    3.18  (*
    3.19    (sym RS real_mult_div_cancel1) handle e => print_exn e;
    3.20  Exception THM 1 raised:

     4.1 --- a/src/Tools/isac/ProgLang/ProgLang.thy	Thu Nov 21 09:18:22 2013 +0100
     4.2 +++ b/src/Tools/isac/ProgLang/ProgLang.thy	Thu Nov 21 11:17:42 2013 +0100
     4.3 @@ -4,9 +4,8 @@
     4.4   *)
     4.5  
     4.6  theory ProgLang imports Script
     4.7 -  uses ("~~/src/Tools/isac/ProgLang/scrtools.sml")
     4.8  begin
     4.9  
    4.10 -use "~~/src/Tools/isac/ProgLang/scrtools.sml"
    4.11 +ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
    4.12  
    4.13  end                       
    4.14 \ No newline at end of file

     5.1 --- a/src/Tools/isac/ProgLang/termC.sml	Thu Nov 21 09:18:22 2013 +0100
     5.2 +++ b/src/Tools/isac/ProgLang/termC.sml	Thu Nov 21 11:17:42 2013 +0100
     5.3 @@ -738,10 +738,10 @@
     5.4    in assbl_thm sign_ref der maxidx shyps hyps (*tpairs*) prop' end;*)
     5.5  fun num_str thm =
     5.6    let val (deriv, 
     5.7 -	   {thy_ref = thy_ref, tags = tags, maxidx = maxidx, shyps = shyps, 
     5.8 +	   {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps, 
     5.9  	    hyps = hyps, tpairs = tpairs, prop = prop}) = rep_thm_G thm
    5.10      val prop' = numbers_to_string prop;
    5.11 -  in assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop' end;
    5.12 +  in assbl_thm deriv thy tags maxidx shyps hyps tpairs prop' end;
    5.13  
    5.14  fun get_thm' xstring = (*?covers 2009 Thm?!, replaces 2002 fun get_thm :
    5.15  val it = fn : theory -> xstring -> Thm.thm*)