1.1 --- a/src/Tools/isac/Interpret/Interpret.thy	Sun Oct 16 13:58:46 2016 +0200
     1.2 +++ b/src/Tools/isac/Interpret/Interpret.thy	Tue Oct 18 12:05:03 2016 +0200
     1.3 @@ -9,6 +9,12 @@
     1.4    ML_file "~~/src/Tools/isac/Interpret/mstools.sml"
     1.5    ML_file "~~/src/Tools/isac/Interpret/ctree.sml"
     1.6    ML_file "~~/src/Tools/isac/Interpret/ptyps.sml"
     1.7 +ML {*
     1.8 +Rewrite';           (*thm' vvv*)
     1.9 +fun thm'_to_thm'' ((thmID, str) : thm') = (thmID, str2term str) : thm'' (*TODO: id + remove*)
    1.10 +fun thm''_to_thm' ((thmID, trm) : thm'') = (thmID, term2str trm) : thm' (*TODO: id + remove*);
    1.11 +Rewrite;           (*thm'' ^^^*)
    1.12 +*}
    1.13    ML_file "~~/src/Tools/isac/Interpret/generate.sml"
    1.14    ML_file "~~/src/Tools/isac/Interpret/calchead.sml"
    1.15    ML_file "~~/src/Tools/isac/Interpret/appl.sml"