tuned

repaired fun nxt_specify_

fun geti_ct converts a term back to a string (for good reasons).
this string got a markup and could not be parsed again.

TODO: check all Syntax.string_of_term for similar cases.

intermed. test/../integrate.sml in -- me method [diff,integration] --

removed last error by
find . -type f -exec sed -i s/"\"Isac.thy\""/"\"Isac\""/g {} \;
find . -type f -exec sed -i s/" Isac.thy"/" (theory \"Isac\")"/g {} \;

intermed. test/../integrate.sml, pbl, met, scr seem to work

error *** ME_Isa: thy 'Isac.thy' not in system
raised in --- me method [diff,integration] ---
before: query-replace Isac.thy

rewriting in test/../integrate.sml works, too

Added working Isac-Scala-jEdit-scr!!!

repaired 'fun calc_equ' for "op <", completed rewriting in test/../rational.sml

TODO:
# delete !theory' and repair related code (Isac.thy !)
# make_thm needs Trueprop $
# ?rename RationalI ?

renamed "op <" to "Orderings.ord_class.less" etc

find . -type f -exec sed -i s/"\"op <\""/"\"Orderings.ord_class.less\""/g {} \;
find . -type f -exec sed -i s/"\"op <=\""/"\"Orderings.ord_class.less_eq\""/g {} \;

intermed. test/../rational.sml, before "op *" --> "Orderings.ord_class.less"

updated print_exn

find . -type f -exec sed -i s/"print_exn "/"OldGoals.print_exn "/g {} \;
TODO: review fun print_exn_G and handle _