1.1 --- a/src/Tools/isac/Interpret/Interpret.thy Tue Oct 18 12:05:03 2016 +0200
1.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Thu Oct 20 10:26:29 2016 +0200
1.3 @@ -9,12 +9,6 @@
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"