1.1 --- a/src/Tools/isac/BaseDefinitions/parseC.sml	Mon Jan 30 09:47:18 2023 +0100
     1.2 +++ b/src/Tools/isac/BaseDefinitions/parseC.sml	Mon Jan 30 12:11:40 2023 +0100
     1.3 @@ -4,8 +4,8 @@
     1.4  *)
     1.5  signature PARSE_ISAC =
     1.6  sig
     1.7 +  val term_position: Proof.context -> string * Position.T -> term
     1.8    val pattern_position: Proof.context -> string * Position.T -> term
     1.9 -  val term_position: Proof.context -> string * Position.T -> term
    1.10  
    1.11    val term_opt: Proof.context -> string -> term option
    1.12    val patt_opt: theory -> string -> term option

     2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Mon Jan 30 09:47:18 2023 +0100
     2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Mon Jan 30 12:11:40 2023 +0100
     2.3 @@ -72,13 +72,11 @@
     2.4  
     2.5    val matches: theory -> term -> term -> bool
     2.6  
     2.7 -  val parse: Proof.context -> string -> term
     2.8 -  val parse_patt: theory -> string -> term
     2.9 +(*val parse_patt: theory -> string -> term              \<longrightarrow> ParseC.patt_opt *)
    2.10  (*val parse_opt: Proof.context -> string -> term option (*kept while developing Specify*)*)
    2.11    val parseNEW: Proof.context -> string -> term option
    2.12    val parseNEW': Proof.context -> string -> term      (*old version to be eliminated*)
    2.13    val parseNEW'': theory -> string -> term            (*old version to be eliminated*)
    2.14 -  (*for test/* *)
    2.15  
    2.16    val str_of_free_opt: term -> string option
    2.17    val str_of_int: int -> string
    2.18 @@ -528,8 +526,6 @@
    2.19    | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
    2.20  (*\----- old versions to be eliminated -------------------------------------------------------/*)
    2.21  
    2.22 -(* to be replaced by Syntax.read_term..*)
    2.23 -fun parse ctxt str = Syntax.read_term_global (Proof_Context.theory_of ctxt) str;
    2.24  (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation *)
    2.25  fun parse_patt thy str = (thy, str)
    2.26    |>> Proof_Context.init_global

     3.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Mon Jan 30 09:47:18 2023 +0100
     3.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Mon Jan 30 12:11:40 2023 +0100
     3.3 @@ -373,7 +373,8 @@
     3.4        let
     3.5          val ctxt = Ctree.get_ctxt pt pos
     3.6          val (pt, c) = Ctree.cappend_atomic pt p l
     3.7 -          (TermC.parse ctxt f) (Tactic.Tac id) (TermC.parse ctxt f', []) Ctree.Complete
     3.8 +          (ParseC.term_opt ctxt f |> the) (Tactic.Tac id) (ParseC.term_opt ctxt f' |> the, [])
     3.9 +            Ctree.Complete
    3.10        in
    3.11          ((p,Pos.Res), c, Test_Out.FormKF f', pt)
    3.12        end

     4.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Mon Jan 30 09:47:18 2023 +0100
     4.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Mon Jan 30 12:11:40 2023 +0100
     4.3 @@ -58,10 +58,10 @@
     4.4  (* function for handling the cas-input "solve (x+1=2, x)":
     4.5     make a model which is already in ctree-internal format *)
     4.6  fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ eq $ bdv] =
     4.7 -    [((TermC.parse \<^context>) "equality", [eq]),
     4.8 -     ((TermC.parse \<^context>) "solveFor", [bdv]),
     4.9 -     ((TermC.parse \<^context>) "solutions", 
    4.10 -      [(TermC.parse \<^context>) "L"])
    4.11 +    [(ParseC.term_opt \<^context> "equality" |> the, [eq]),
    4.12 +     (ParseC.term_opt \<^context> "solveFor" |> the, [bdv]),
    4.13 +     (ParseC.term_opt \<^context> "solutions" |> the, 
    4.14 +      [ParseC.term_opt\<^context> "L" |> the])
    4.15       ]
    4.16    | argl2dtss _ = raise ERROR "Equation.ML: wrong argument for argl2dtss";
    4.17  \<close>

     5.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Mon Jan 30 09:47:18 2023 +0100
     5.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Mon Jan 30 12:11:40 2023 +0100
     5.3 @@ -110,7 +110,8 @@
     5.4  val dummyT = TFree ("'a", ["HOL.type"]);
     5.5  
     5.6  fun subst_adapt_to_type ctxt subst = (subst
     5.7 -  |> map (TermC.parse ctxt)
     5.8 +  |> map (ParseC.term_opt ctxt)
     5.9 +  |> map the
    5.10    |> map TermC.isapair2pair (*replace by HOLogic.strip_tuple etc*)
    5.11    |> map (apfst HOLogic.dest_string)
    5.12    |> map (apfst (fn str => (TermC.mk_Free (str, dummyT))))

     6.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy	Mon Jan 30 09:47:18 2023 +0100
     6.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy	Mon Jan 30 12:11:40 2023 +0100
     6.3 @@ -196,17 +196,17 @@
     6.4  
     6.5  (* check if a term is a Prog_Tac *)
     6.6  
     6.7 -val Calculate = TermC.parse @{context} "Calculate";
     6.8 -val Rewrite = TermC.parse @{context} "Rewrite";
     6.9 -val Rewrite_Inst = TermC.parse @{context} "Rewrite'_Inst";
    6.10 -val Rewrite_Set = TermC.parse @{context} "Rewrite'_Set";
    6.11 -val Rewrite_Set_Inst = TermC.parse @{context} "Rewrite'_Set'_Inst";
    6.12 -val Or_to_List = TermC.parse @{context} "Or'_to'_List";
    6.13 -val SubProblem = TermC.parse @{context} "SubProblem";
    6.14 -val Substitute = TermC.parse @{context} "Substitute";
    6.15 -val Take = TermC.parse @{context} "Take";
    6.16 -val Check_elementwise = TermC.parse @{context} "Check'_elementwise";
    6.17 -val Assumptions = TermC.parse @{context} "Assumptions";
    6.18 +val SOME Calculate = ParseC.term_opt @{context} "Calculate";
    6.19 +val SOME Rewrite = ParseC.term_opt @{context} "Rewrite";
    6.20 +val SOME Rewrite_Inst = ParseC.term_opt @{context} "Rewrite'_Inst";
    6.21 +val SOME Rewrite_Set = ParseC.term_opt @{context} "Rewrite'_Set";
    6.22 +val SOME Rewrite_Set_Inst = ParseC.term_opt @{context} "Rewrite'_Set'_Inst";
    6.23 +val SOME Or_to_List = ParseC.term_opt @{context} "Or'_to'_List";
    6.24 +val SOME SubProblem = ParseC.term_opt @{context} "SubProblem";
    6.25 +val SOME Substitute = ParseC.term_opt @{context} "Substitute";
    6.26 +val SOME Take = ParseC.term_opt @{context} "Take";
    6.27 +val SOME Check_elementwise = ParseC.term_opt @{context} "Check'_elementwise";
    6.28 +val SOME Assumptions = ParseC.term_opt @{context} "Assumptions";
    6.29  
    6.30  val all_Consts = [Calculate, Rewrite, Rewrite_Inst, Rewrite_Set, Rewrite_Set_Inst, Or_to_List,
    6.31    SubProblem, Substitute, Take, Check_elementwise, Assumptions]
    6.32 @@ -224,9 +224,10 @@
    6.33    Remarkably this appears not necessary for \<open>Rewrite_Inst\<close> and \<open>Rewrite_Set_Inst\<close>;
    6.34    for these, hoewever, \<open>adapt_to_type\<close> is required for conversion from \<open>Tac.subst_input\<close>.
    6.35  *)
    6.36 -(* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type *)
    6.37 +(* ParseC.term_opt ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type *)
    6.38  fun Take_adapt_to_type ctxt arg = arg
    6.39 -  |> TermC.parse ctxt
    6.40 +  |> ParseC.term_opt ctxt
    6.41 +  |> the
    6.42    |> ParseC.adapt_term_to_type ctxt
    6.43  
    6.44  fun Substitute_adapt_to_type thy isasub =
    6.45 @@ -237,7 +238,8 @@
    6.46  
    6.47  (* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type *)
    6.48  fun Substitute_adapt_to_type' ctxt strs = strs
    6.49 -  |> map (TermC.parse ctxt)
    6.50 +  |> map (ParseC.term_opt ctxt)
    6.51 +  |> map the
    6.52    |> map (ParseC.adapt_term_to_type ctxt)
    6.53  
    6.54  (**)end(*struct*)

     7.1 --- a/src/Tools/isac/ProgLang/Tactical.thy	Mon Jan 30 09:47:18 2023 +0100
     7.2 +++ b/src/Tools/isac/ProgLang/Tactical.thy	Mon Jan 30 12:11:40 2023 +0100
     7.3 @@ -33,13 +33,13 @@
     7.4  struct
     7.5  (**)
     7.6  
     7.7 -val (Let $ _ $ _) = TermC.parse @{context} "let aaa = 1 in aaa"
     7.8 -val (Chain) = TermC.parse @{context} "Chain";
     7.9 -val (Try) = TermC.parse @{context} "Try";
    7.10 -val (Repeat) = TermC.parse @{context} "Repeat";
    7.11 -val (Or $ _ $ _) = TermC.parse @{context} "aaa Or bbb";
    7.12 -val (While $ _ $ _) = TermC.parse @{context} "While aaa Do bbb";
    7.13 -val (If $ _ $ _ $ _) = TermC.parse @{context} "If aaa Then bbb Else ccc";
    7.14 +val SOME (Let $ _ $ _) = ParseC.term_opt @{context} "let aaa = 1 in aaa"
    7.15 +val SOME (Chain) = ParseC.term_opt @{context} "Chain";
    7.16 +val SOME (Try) = ParseC.term_opt @{context} "Try";
    7.17 +val SOME (Repeat) = ParseC.term_opt @{context} "Repeat";
    7.18 +val SOME (Or $ _ $ _) = ParseC.term_opt @{context} "aaa Or bbb";
    7.19 +val SOME (While $ _ $ _) = ParseC.term_opt @{context} "While aaa Do bbb";
    7.20 +val SOME (If $ _ $ _ $ _) = ParseC.term_opt @{context} "If aaa Then bbb Else ccc";
    7.21  
    7.22  val all_Consts = [Let, Chain, Try, Repeat, Or, While, If]
    7.23  

     8.1 --- a/src/Tools/isac/Specify/Input_Descript.thy	Mon Jan 30 09:47:18 2023 +0100
     8.2 +++ b/src/Tools/isac/Specify/Input_Descript.thy	Mon Jan 30 12:11:40 2023 +0100
     8.3 @@ -174,7 +174,12 @@
     8.4    let val elems = (flat o (map TermC.isalist2list)) ts;
     8.5    in TermC.list2isalist (type_of (hd elems)) elems end;
     8.6  
     8.7 -val script_parse = @{theory BaseDefinitions} |> Proof_Context.init_global |> TermC.parse;
     8.8 +fun script_parse str =
     8.9 +  let
    8.10 +    val ctxt = @{theory BaseDefinitions} |> Proof_Context.init_global
    8.11 +  in
    8.12 +    ParseC.term_opt ctxt str |> the
    8.13 +  end;
    8.14  val e_listReal = script_parse "[]::(real list)";
    8.15  val e_listBool = script_parse "[]::(bool list)";
    8.16  
    8.17 @@ -187,7 +192,6 @@
    8.18  	    else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b] *)
    8.19  	  else (hd ts)               (* a variable or metavariable for a list *)
    8.20    else (hd ts);
    8.21 -(* *)
    8.22  fun join (d, []) = 
    8.23    	if for_real_list d
    8.24    	then (d $ e_listReal)

     9.1 --- a/src/Tools/isac/Specify/cas-command.sml	Mon Jan 30 09:47:18 2023 +0100
     9.2 +++ b/src/Tools/isac/Specify/cas-command.sml	Mon Jan 30 12:11:40 2023 +0100
     9.3 @@ -104,7 +104,9 @@
     9.4        Parse.!!! (Parse.ML_source -- parse_theory -- parse_problem -- parse_method))
     9.5        >> (fn (term, (((source, thry), pbl), met)) => Toplevel.theory (fn thy =>
     9.6          let
     9.7 -          val t = TermC.parse (Proof_Context.init_global thy) term;
     9.8 +        (*/------------ replace by ParseC.term_position ------------------\*)
     9.9 +          val SOME t = ParseC.term_opt (Proof_Context.init_global thy) term;
    9.10 +        (*\------------ replace by ParseC.term_position ------------------/*)
    9.11            val pblID = References_Def.explode_id pbl;
    9.12            val metID = References_Def.explode_id met;
    9.13            val set_data =

    10.1 --- a/src/Tools/isac/Specify/i-model.sml	Mon Jan 30 09:47:18 2023 +0100
    10.2 +++ b/src/Tools/isac/Specify/i-model.sml	Mon Jan 30 12:11:40 2023 +0100
    10.3 @@ -252,8 +252,10 @@
    10.4  fun check_single ctxt m_field [] i_model m_patt (ct(*, pos*)) =
    10.5      let
    10.6        val i = 1 + (if i_model = [] then 0 else map #1 i_model |> maxl)
    10.7 -      val t = TermC.parse ctxt ct
    10.8 +    (*/------------ replace by ParseC.term_position -----------\*)
    10.9 +      val t = Syntax.read_term ctxt ct
   10.10          handle ERROR msg => error (msg (*^ Position.here pos*))
   10.11 +    (*\------------ replace by ParseC.term_position -----------/*)
   10.12          (*NONE => Add (i, [], false, m_field, Syn ct)*)
   10.13        val (d, ts) = Input_Descript.split t
   10.14      in 

    11.1 --- a/src/Tools/isac/Specify/p-spec.sml	Mon Jan 30 09:47:18 2023 +0100
    11.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Mon Jan 30 12:11:40 2023 +0100
    11.3 @@ -223,7 +223,7 @@
    11.4        val thy = Know_Store.get_via_last_thy dI
    11.5  (** ) val ctxt = Proof_Context.init_global (ThyC.get_theory sdI)( **)
    11.6      in if CAS_Cmd.is_from hdf fmz
    11.7 -       then the (CAS_Cmd.input (TermC.parse (Proof_Context.init_global thy) hdf)) 
    11.8 +       then the (CAS_Cmd.input (ParseC.term_opt (Proof_Context.init_global thy) hdf |> the)) 
    11.9         else
   11.10           let val (pos_, pits, mits) = 
   11.11  	         if dI <> sdI