1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Wed Sep 29 18:56:38 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Wed Sep 29 19:26:12 2021 +0200
     1.3 @@ -74,7 +74,6 @@
     1.4    val parseNEW: Proof.context -> string -> term option
     1.5    val parseNEW': Proof.context -> string -> term
     1.6    val parseNEW'': theory -> string -> term
     1.7 -  val parseold: theory -> string -> cterm option
     1.8    val parseN: theory -> string -> cterm option
     1.9    val parse_strict: theory -> string -> term
    1.10    val parse: theory -> string -> cterm option
    1.11 @@ -557,10 +556,6 @@
    1.12    | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
    1.13  
    1.14  (* TODO clarify parse with Test_Isac *)
    1.15 -fun parseold thy str = (* before 2002 *)
    1.16 -  \<^try>\<open>
    1.17 -    let val t = Syntax.read_term_global thy str
    1.18 -    in Thm.global_cterm_of thy t end\<close>;
    1.19  fun parseN thy str = (* introduced 2002 *)
    1.20    \<^try>\<open>
    1.21      let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)

     2.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Wed Sep 29 18:56:38 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Wed Sep 29 19:26:12 2021 +0200
     2.3 @@ -36,7 +36,7 @@
     2.4  val chkorg = map (the o (parse thy)) org;
     2.5  val pbl = {given=["fixedValues [R=(R::real)]"],where_=[],
     2.6  	   find=["maximum A", "values_for [a,b]"],
     2.7 -	   with_=[(* incompat.w. parse, ok with parseold
     2.8 +	   with_=[(* incompat.w. parse, ok with parseold: theory -> string -> cterm option
     2.9  		   "EX alpha. A=#2*a*b - a \<up> #2 &    \
    2.10  	    \ a=#2*R*sin alpha & b=#2*R*cos alpha & \
    2.11  	    \ (ALL A'. A'=#2*a*b - a \<up> #2 & a=#2*R*sin alpha \
    2.12 @@ -53,7 +53,7 @@
    2.13  	   where_=[],
    2.14  	   find=["maximum m", "valuesFor (ms::bool list)",
    2.15  		 "function_term t", "max_argument mx"],
    2.16 -	   with_=[(* incompat.w. parse, ok with parseold
    2.17 +	   with_=[(* incompat.w. parse, ok with parseold: theory -> string -> cterm option
    2.18  		   "Ex_frees ((foldl (op &) True (mr#ars)) &           \
    2.19                    \ (ALL m'. (subst (m,m') (foldl (op &) True (mr#ars))\
    2.20  		  \            --> m' <= m))) &                        \
    2.21 @@ -71,7 +71,7 @@
    2.22  	   where_=[],
    2.23  	   find=["maximum A", "valuesFor [a=Undef]",
    2.24  		 "function_term t", "max_argument mx"],
    2.25 -	   with_=[(* incompat.w. parse, ok with parseold
    2.26 +	   with_=[(* incompat.w. parse, ok with parseold: theory -> string -> cterm option
    2.27  		   "EX b alpha. A = #2*a*b - a \<up> #2 &     \
    2.28  	            \          a = #2*R*sin alpha  &     \
    2.29  		    \          b = #2*R*cos alpha  &     \
    2.30 @@ -85,6 +85,7 @@
    2.31  		   "additionalRels ars"]}: string ppc;
    2.32  val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) met;
    2.33  
    2.34 +parseold: theory -> string -> cterm option;
    2.35  val (SOME ct) = parseold thy "EX b. (EX alpha. A = #2*a*b - a \<up> #2)";
    2.36  
    2.37  "pbltyp --- make_fun ---";
    2.38 @@ -123,7 +124,7 @@
    2.39  		     "domain {x::real. lower_bound <= x & x <= upper_bound}"],
    2.40  	      where_=[],
    2.41  	      find=["maximums ms"],
    2.42 -	      with_=[(* incompat.w. parse, ok with parseold
    2.43 +	      with_=[(* incompat.w. parse, ok with parseold: theory -> string -> cterm option
    2.44  		   "ALL m. m : ms --> \
    2.45  	          \  (ALL x::real. lower_bound <= x & x <= upper_bound \
    2.46  	          \        --> (%v. t) x <= m)"*)],
    2.47 @@ -198,7 +199,7 @@
    2.48  val where_ = ["lhs is_atom", "bdv is_atom", "low is_atom", "high is_atom",
    2.49  	      "||| Vars equ ||| = ||| VarsSet ac ||| - ||| ac ||| + #1"];
    2.50  val find   = ["f::real => real", "maxs::real set"];
    2.51 -val with_  = [(* incompat.w. parse, ok with parseold
    2.52 +val with_  = [(* incompat.w. parse, ok with parseold: theory -> string -> cterm option
    2.53  		   "maxs = {m. low < m & m < high & \
    2.54                          \ (m is_local_max_of (%bdv. f))}"*)];
    2.55  val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);

     3.1 --- a/src/Tools/isac/Specify/i-model.sml	Wed Sep 29 18:56:38 2021 +0200
     3.2 +++ b/src/Tools/isac/Specify/i-model.sml	Wed Sep 29 19:26:12 2021 +0200
     3.3 @@ -209,7 +209,7 @@
     3.4  
     3.5  fun vars_of itms = itms |> mk_env |> map snd
     3.6  
     3.7 -val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow";
     3.8 +val dsc_unknown = TermC.parseNEW'' @{theory} "unknown::'a => unknow";
     3.9  
    3.10  (* get a term from ori, notyet input in itm.
    3.11     the term from ori is thrown back to a string in order to reuse