1.1 --- a/TODO.md Wed Oct 26 09:54:58 2022 +0200
1.2 +++ b/TODO.md Mon Oct 31 16:43:48 2022 +0100
1.3 @@ -38,6 +38,9 @@
1.4 How can Scan.* be traced?
1.5 (Tracing should help understanding Problem.parse_cas, Problem.parse_model_input which involve Scan.* )
1.6
1.7 +* WN ? Problem/MethodC.prep_input: model_input UNDERGOES Parse.term in parse_tagged_terms
1.8 + AND AGAIN UNDERGOES Syntax.read_term_global IN prep_input
1.9 +
1.10 * postpone: ?How accomplish two user-requirements by Outer_Syntax.command \<^command_keyword>\<open>Example\<close>
1.11 (1) start a Calculation with a CAS_Cmd
1.12 (2) start an Example from scratch, i.e. with (Formalize.empty, References.empty)
1.13 @@ -47,7 +50,8 @@
1.14
1.15 ***** priority of WN items is top down, most urgent/simple on top
1.16
1.17 -* WN: review Problem/MethodC..prep_input, improve after conference with MW
1.18 +* WN?: improve Problem/MethodC..prep_input after meeting MW: parse twice?
1.19 +* WN: rename fields in Problem_def.T
1.20 * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store›
1.21 * WN: KEStore_Elems.get_thes, add_thes still required for Error_Patterns, we want to eliminate thes:
1.22 (1) Error_Pattern.T are already stored by MethodC -- place them in respective thys
2.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Oct 26 09:54:58 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Mon Oct 31 16:43:48 2022 +0100
2.3 @@ -30,13 +30,13 @@
2.4 ML_file "eval-def.sml"
2.5 ML_file "rewrite-order.sml"
2.6 ML_file rule.sml
2.7 +ML_file "references-def.sml"
2.8 ML_file "model-pattern.sml"
2.9 ML_file "error-pattern-def.sml"
2.10 ML_file "rule-set.sml"
2.11
2.12 ML_file "store.sml"
2.13 ML_file "check-unique.sml"
2.14 -ML_file "references-def.sml"
2.15 ML_file "problem-def.sml"
2.16 ML_file "method-def.sml"
2.17 ML_file "cas-def.sml"
3.1 --- a/src/Tools/isac/BaseDefinitions/model-pattern.sml Wed Oct 26 09:54:58 2022 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/model-pattern.sml Mon Oct 31 16:43:48 2022 +0100
3.3 @@ -14,6 +14,11 @@
3.4 val to_string: single list -> string
3.5 type m_field = string
3.6 type descriptor = term
3.7 + val split_descriptor: Proof.context -> term -> descriptor * term
3.8 + val parse_split_items: Proof.context -> References_Def.id -> m_field ->
3.9 + (m_field * (*TermC.as_*)string list) list -> T
3.10 + val parse_items: Proof.context -> References_Def.id ->
3.11 + (m_field * (*TermC.as_*)string list) list -> single list * single list * single list * term list
3.12
3.13 val variables: T -> term list
3.14 val get_field: descriptor -> T -> m_field option
3.15 @@ -42,6 +47,44 @@
3.16 term)) (* id | arbitrary term *);
3.17 type T = single list;
3.18
3.19 +fun split_descriptor ctxt dsc_tm =
3.20 + let
3.21 + val (hd, arg) = case strip_comb dsc_tm of
3.22 + (hd, [arg]) => (hd, arg)
3.23 + | _ => raise ERROR ("Model_Pattern.split_descriptor: doesn't match (hd,[arg]) for t = " ^
3.24 + quote (UnparseC.term_in_ctxt ctxt dsc_tm))
3.25 + in (hd, arg) end
3.26 +fun parse_split_items ctxt pbl_id m_field model_input =
3.27 + let
3.28 + val items = filter ((fn f => (fn (f', _) => f = f')) m_field) model_input
3.29 + val items' = case items of
3.30 + [] => []
3.31 + | ((_, items'') :: []) =>
3.32 + map (split_descriptor ctxt o
3.33 + (Syntax.read_term_global (Proof_Context.theory_of ctxt))) items''
3.34 + | _ =>
3.35 + raise ERROR ("Model_Pattern.parse_split_items: more than one " ^ quote m_field ^
3.36 + " in " ^ quote (References_Def.id_to_string pbl_id))
3.37 + in
3.38 + map (pair m_field) items'
3.39 + end
3.40 +fun parse_items ctxt pbl_id model_input =
3.41 + let
3.42 + val gi = parse_split_items ctxt pbl_id "#Given" model_input;
3.43 + val fi = parse_split_items ctxt pbl_id "#Find" model_input;
3.44 + val re = parse_split_items ctxt pbl_id "#Relate" model_input;
3.45 +
3.46 + val wh = filter ((fn f => (fn (f', _) => f = f')) "#Where") model_input;
3.47 + val wh = (case wh of
3.48 + [] => []
3.49 + | ((_, wh') :: []) => map (Proof_Context.read_term_pattern ctxt) wh'
3.50 + | _ =>
3.51 + raise ERROR ("prep_input: more than one " ^ quote "#Where" ^
3.52 + " in " ^ quote (References_Def.id_to_string pbl_id)))
3.53 + in
3.54 + (gi, fi, re, wh)
3.55 + end;
3.56 +
3.57 fun pat2str (field, (dsc, id)) = pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id));
3.58 fun to_string pats = (strs2str o (map pat2str)) pats;
3.59 \<^isac_test>\<open>
4.1 --- a/src/Tools/isac/BaseDefinitions/problem-def.sml Wed Oct 26 09:54:58 2022 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/problem-def.sml Mon Oct 31 16:43:48 2022 +0100
4.3 @@ -33,17 +33,20 @@
4.4 type T =
4.5 {guh : Check_Unique.id, (* unique within Isac_Knowledge, for html-presentation *)
4.6 mathauthors : string list, (* copyright *)
4.7 +(*start_refine: References_Def.id,*)
4.8 init : References_Def.id, (* to start refinement with *)
4.9 - thy : theory, (* which allows to compile that T
4.10 - TODO: search generalized for subthy (ref.p.69*)
4.11 + thy : theory, (* which allows to compile that T *)
4.12 (*^^^ WN050912 NOT used during application of the problem,
4.13 because applied terms may be from 'subthy' as well as from super;
4.14 thus we take 'maxthy'; see match_ags ! *)
4.15 cas : term option, (* CAS_Cmd *)
4.16 +(*solve_mets: References_Def.id list,*)
4.17 met : References_Def.id list, (* methods solving the T *)
4.18 +(*where_rls: Rule_Set.T,*)
4.19 prls : Rule_Set.T, (* for evaluation of preconditions in "#Where" on "#Given" *)
4.20 where_ : term list, (* ? DEL, as soon as they are input interactively ? *)
4.21 - ppc : Model_Pattern.T (* contains "#Given", "#Where", "#Find", "#Relate"
4.22 +(*model: Model_Pattern.T*)
4.23 + ppc : Model_Pattern.T (* contains "#Given", "#Find", "#Relate"
4.24 for constraints on identifiers see "O_Model.copy_name" *)
4.25 }
4.26 val empty = {guh = "pbl_empty", mathauthors = [], init = id_empty, thy = @{theory "Pure"},
5.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Oct 26 09:54:58 2022 +0200
5.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Mon Oct 31 16:43:48 2022 +0100
5.3 @@ -20,12 +20,12 @@
5.4 "CAS" "Program" "Given" "Where" "Find" "Relate"
5.5 begin
5.6 ML_file thmC.sml
5.7 + ML_file "model-def.sml"
5.8 ML_file problem.sml
5.9 ML_file method.sml
5.10
5.11 ML_file rewrite.sml
5.12
5.13 - ML_file "model-def.sml"
5.14 ML_file "istate-def.sml"
5.15 ML_file "calc-tree-elem.sml"
5.16 ML_file "pre-conds-def.sml"
6.1 --- a/src/Tools/isac/MathEngBasic/method.sml Wed Oct 26 09:54:58 2022 +0200
6.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Mon Oct 31 16:43:48 2022 +0100
6.3 @@ -19,7 +19,6 @@
6.4 val id_to_string: id -> string
6.5
6.6 type input
6.7 - (* TODO: ------------ remove always empty --- vvvvvvvvvvv -- vvv*)
6.8 val prep_input: theory -> Check_Unique.id -> string list -> id ->
6.9 id * Problem.model_input * input * thm -> T * id
6.10
6.11 @@ -50,58 +49,19 @@
6.12 {calc: Rule_Def.eval_ml_from_prog list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,
6.13 prls: Rule_Set.T, rew_ord': Rewrite_Ord.id, rls': Rule_Set.T, srls: Rule_Set.T}
6.14
6.15 -fun prep_input thy guh (mathauthors: string list) (init: References_Def.id)
6.16 - (metID, ppc,
6.17 - {rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr,
6.18 - errpats = ep, nrls = nr}, scr) =
6.19 - let
6.20 - fun eq f (f', _) = f = f';
6.21 - val gi = filter (eq "#Given") ppc;
6.22 - val gi = (case gi of
6.23 - [] => (writeln ("prep_input: in " ^ guh ^ " #Given is empty ?!?"); [])
6.24 - | ((_, gi') :: []) =>
6.25 - (*(case \<^try>\<open> *)map (Problem.split_did o (Syntax.read_term_global thy)) gi'(*\<close> of
6.26 - SOME x => x
6.27 - | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))*)
6.28 - | _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str metID));
6.29 - val gi = map (pair "#Given") gi;
6.30 -
6.31 - val fi = filter (eq "#Find") ppc;
6.32 - val fi = (case fi of
6.33 - [] => (writeln ("prep_input: in " ^ guh ^ " #Find is empty ?!?"); [])
6.34 - | ((_, fi') :: []) =>
6.35 - (*(case \<^try>\<open> *)map (Problem.split_did o (Syntax.read_term_global thy)) fi'(*\<close> of
6.36 - SOME x => x
6.37 - | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))*)
6.38 - | _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str metID));
6.39 - val fi = map (pair "#Find") fi;
6.40 -
6.41 - val re = filter (eq "#Relate") ppc;
6.42 - val re = (case re of
6.43 - [] => (writeln ("prep_input: in " ^ guh ^ " #Relate is empty ?!?"); [])
6.44 - | ((_,re') :: []) =>
6.45 - (*(case \<^try>\<open> *) map (Problem.split_did o (Syntax.read_term_global thy)) re'(*\<close> of
6.46 - SOME x => x
6.47 - | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))*)
6.48 - | _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));
6.49 - val re = map (pair "#Relate") re;
6.50 -
6.51 - val wh = filter (eq "#Where") ppc;
6.52 - val wh = (case wh of
6.53 - [] => (writeln ("prep_input: in " ^ guh ^ " #Where is empty ?!?"); [])
6.54 - | ((_, wh') :: []) =>
6.55 - (*(case \<^try>\<open> *)map (TermC.parse_patt thy) wh'(*\<close> of
6.56 - SOME x => x
6.57 - | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Where' of " ^ strs2str metID))*)
6.58 - | _ => raise ERROR ("prep_pbt: more than one '#Where' in " ^ strs2str metID));
6.59 - val sc = Program.prep_program scr
6.60 - val calc = if Thm.eq_thm (scr, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc
6.61 - in
6.62 - ({guh = guh, mathauthors = mathauthors, init = init, ppc = gi @ fi @ re, pre = wh,
6.63 - rew_ord' = ro, erls = rls, srls = srls, prls = prls, calc = calc,
6.64 - crls = cr, errpats = ep, nrls = nr, scr = Rule.Prog sc}, metID)
6.65 - end;
6.66 -
6.67 +fun prep_input thy guh mathauthors start_refine (met_id, model_input,
6.68 + {rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr,
6.69 + errpats = ep, nrls = nr}, prog) =
6.70 + let
6.71 + val ctxt = Proof_Context.init_global thy
6.72 + val (gi, fi, re, wh) = Model_Pattern.parse_items ctxt met_id model_input
6.73 + val sc = Program.prep_program prog
6.74 + val calc = if Thm.eq_thm (prog, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc
6.75 + in
6.76 + ({guh = guh, mathauthors = mathauthors, init = start_refine, ppc = gi @ fi @ re, pre = wh,
6.77 + rew_ord' = ro, erls = rls, srls = srls, prls = prls, calc = calc,
6.78 + crls = cr, errpats = ep, nrls = nr, scr = Rule.Prog sc}, met_id)
6.79 + end;
6.80
6.81 (** Isar command **)
6.82
7.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Wed Oct 26 09:54:58 2022 +0200
7.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Mon Oct 31 16:43:48 2022 +0100
7.3 @@ -21,8 +21,6 @@
7.4
7.5 type input
7.6 type model_input
7.7 - val split_did: term -> term * term
7.8 - (* TODO: ---------- remove always empty ----- vvvvvvvvvvv -- vvv*)
7.9 val prep_input: theory -> Check_Unique.id -> string list -> id -> input -> T * id
7.10
7.11 val set_data: Rule_Def.rule_set -> theory -> theory
7.12 @@ -76,60 +74,18 @@
7.13 TermC.as_string option * (* CAS_Cmd *)
7.14 Meth_Def.id list; (* methods that can solve the problem *)
7.15
7.16 -(* split a term into description and (id | structured variable) for pbt, met.ppc *)
7.17 -fun split_did t =
7.18 - let
7.19 - val (hd, arg) = case strip_comb t of
7.20 - (hd, [arg]) => (hd, arg)
7.21 - | _ => raise ERROR ("split_did: doesn't match (hd,[arg]) for t = xxxxx" (*^ UnparseC.term t*))
7.22 - in (hd, arg) end
7.23 -
7.24 (* prepare problem-types before storing in pbltypes;
7.25 dont forget to "check_guh_unique" before inserting *)
7.26 -fun prep_input thy guh maa init (pblID, dsc_dats, ev, ca, metIDs) =
7.27 - let
7.28 - fun eq f (f', _) = f = f';
7.29 - val gi = filter (eq "#Given") dsc_dats;
7.30 - val gi = (case gi of
7.31 - [] => []
7.32 - | ((_, gi') :: []) =>
7.33 - map (split_did o (Syntax.read_term_global thy)) gi'
7.34 - | _ => raise ERROR ("prep_input: more than one '#Given' in xxxxx" (*^ strs2str pblID*)));
7.35 - val gi = map (pair "#Given") gi;
7.36 -
7.37 - val fi = filter (eq "#Find") dsc_dats;
7.38 - val fi = (case fi of
7.39 - [] => []
7.40 - | ((_, fi') :: []) =>
7.41 - (*(case \<^try>\<open> *)map (split_did o (Syntax.read_term_global thy)) fi'(*\<close> of
7.42 - SOME x => x
7.43 - | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Find' of " ^ strs2str pblID))*)
7.44 - | _ => raise ERROR ("prep_input: more than one '#Find' in xxxxx" (*^ strs2str pblID*)));
7.45 - val fi = map (pair "#Find") fi;
7.46 -
7.47 - val re = filter (eq "#Relate") dsc_dats;
7.48 - val re = (case re of
7.49 - [] => []
7.50 - | ((_, re') :: []) =>
7.51 - (*(case \<^try>\<open> *)map (split_did o (Syntax.read_term_global thy)) re'(*\<close> of
7.52 - SOME x => x
7.53 - | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Relate' of " ^ strs2str pblID))*)
7.54 - | _ => raise ERROR ("prep_input: more than one '#Relate' in xxxxx" (*^ strs2str pblID*)));
7.55 - val re = map (pair "#Relate") re;
7.56 -
7.57 - val wh = filter (eq "#Where") dsc_dats;
7.58 - val wh = (case wh of
7.59 - [] => []
7.60 - | ((_, wh') :: []) => (*special case in parsing*)
7.61 - (*(case \<^try>\<open> *)map (TermC.parse_patt thy) wh'(*\<close> of
7.62 - SOME x => x
7.63 - | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Where' of " ^ strs2str pblID))*)
7.64 - | _ => raise ERROR ("prep_input: more than one '#Where' in xxxxx" (*^ strs2str pblID*)));
7.65 - in
7.66 - ({guh = guh, mathauthors = maa, init = init, thy = thy,
7.67 - cas = Option.map (Syntax.read_term_global thy) ca,
7.68 - prls = ev, where_ = wh, ppc = gi @ fi @ re, met = metIDs}, pblID)
7.69 - end;
7.70 +(*??? Syntax.read_term_global below ------+-------vvvvvvvvvvv Parse.term in parse_tagged_terms ???*)
7.71 +fun prep_input thy name maa start_refine (pbl_id, model_input, where_rls, cas, met_ids) =
7.72 + let
7.73 + val ctxt = Proof_Context.init_global thy
7.74 + val (gi, fi, re, wh) = Model_Pattern.parse_items ctxt pbl_id model_input
7.75 + in
7.76 + ({guh = name, mathauthors = maa, init = start_refine, thy = thy,
7.77 + cas = Option.map (Syntax.read_term_global thy) cas,
7.78 + prls = where_rls, where_ = wh, ppc = gi @ fi @ re, met = met_ids}, pbl_id)
7.79 + end;
7.80
7.81
7.82 (** Isar command **)
7.83 @@ -193,8 +149,8 @@
7.84 ML_Context.expression (Input.pos_of source)
7.85 (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")
7.86 |> Context.theory_map;
7.87 - val input = the_data (set_data thy);
7.88 - val arg = prep_input thy name maa id_empty (pblID, model_input, input, cas, metIDs);
7.89 + val where_rls = the_data (set_data thy);
7.90 + val arg = prep_input thy name maa id_empty (pblID, model_input, where_rls, cas, metIDs);
7.91 in KEStore_Elems.add_pbls @{context} [arg] thy end)))
7.92
7.93 in end;
8.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Wed Oct 26 09:54:58 2022 +0200
8.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Mon Oct 31 16:43:48 2022 +0100
8.3 @@ -460,7 +460,7 @@
8.4 *)
8.5 > val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
8.6 val equalities_es_ = "equalities es_" : string
8.7 -> val (dd, ii) = (split_did o Thm.term_of o the o (TermC.parse thy)) equalities_es_;
8.8 +> val (dd, ii) = ((Model_Pattern.split_descriptor ctxt) o Thm.term_of o the o (TermC.parse thy)) equalities_es_;
8.9 > show_types:=true; UnparseC.term ii; show_types:=false;
8.10 val it = "es_::bool list" : string
8.11 ~~~~~~~~~~~~~~~ \<up> \<up> \<up> OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
9.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Wed Oct 26 09:54:58 2022 +0200
9.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Mon Oct 31 16:43:48 2022 +0100
9.3 @@ -122,13 +122,13 @@
9.4 val dsc = Const (\<^const_name>\<open>Input_Descript.solveFor\<close>, "RealDef.real => Tools.una") : term
9.5 val vl = Free ("x", "RealDef.real") : term
9.6
9.7 - val (dsc,id) = (split_did o Thm.term_of o the o (TermC.parse thy)) "solveFor v_";
9.8 + val (dsc,id) = ((Model_Pattern.split_descriptor ctxt) o Thm.term_of o the o (TermC.parse thy)) "solveFor v_";
9.9 pbl_ids ctxt dsc vl;
9.10 val it = [Free ("x", "RealDef.real")] : term list
9.11
9.12 val (dsc,vl) = (Input_Descript.split o Thm.term_of o the o(TermC.parse thy))
9.13 "errorBound (eps=#0)";
9.14 - val (dsc,id) = (split_did o Thm.term_of o the o(TermC.parse thy)) "errorBound err_";
9.15 + val (dsc,id) = ((Model_Pattern.split_descriptor ctxt) o Thm.term_of o the o(TermC.parse thy)) "errorBound err_";
9.16 pbl_ids ctxt dsc vl;
9.17 val it = [Free ("#0", "RealDef.real"),Free ("eps", "RealDef.real")] : term list *)
9.18 "----------- fun upd_penv ----------------------------------------------------------------------";
9.19 @@ -136,15 +136,15 @@
9.20 "----------- fun upd_penv ----------------------------------------------------------------------";
9.21 (*
9.22 val penv = [];
9.23 - val (dsc,vl) = (split_did o Thm.term_of o the o (TermC.parse thy)) "solveFor x";
9.24 - val (dsc,id) = (split_did o Thm.term_of o the o (TermC.parse thy)) "solveFor v_";
9.25 + val (dsc,vl) = ((Model_Pattern.split_descriptor ctxt) o Thm.term_of o the o (TermC.parse thy)) "solveFor x";
9.26 + val (dsc,id) = ((Model_Pattern.split_descriptor ctxt) o Thm.term_of o the o (TermC.parse thy)) "solveFor v_";
9.27 val penv = upd_penv thy penv dsc (id, vl);
9.28 [(Free ("v_", "RealDef.real"),
9.29 [Const (#,#) $ Free (#,#) $ Free ("#0", "RealDef.real")])]
9.30 : (term * term list) list
9.31
9.32 - val (dsc,vl) = (split_did o Thm.term_of o the o(TermC.parse thy))"errorBound (eps=#0)";
9.33 - val (dsc,id) = (split_did o Thm.term_of o the o(TermC.parse thy))"errorBound err_";
9.34 + val (dsc,vl) = ((Model_Pattern.split_descriptor ctxt) o Thm.term_of o the o(TermC.parse thy))"errorBound (eps=#0)";
9.35 + val (dsc,id) = ((Model_Pattern.split_descriptor ctxt) o Thm.term_of o the o(TermC.parse thy))"errorBound err_";
9.36 upd_penv thy penv dsc (id, vl);
9.37 [(Free ("v_", "RealDef.real"),
9.38 [Const (#,#) $ Free (#,#) $ Free ("#0", "RealDef.real")]),
9.39 @@ -158,8 +158,8 @@
9.40 (*
9.41 val i = 2;
9.42 val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;
9.43 - val (dsc,vl) = (split_did o Thm.term_of o the o(TermC.parse thy))"boundVariable b";
9.44 - val (dsc,id) = (split_did o Thm.term_of o the o(TermC.parse thy))"boundVariable v_";
9.45 + val (dsc,vl) = ((Model_Pattern.split_descriptor ctxt) o Thm.term_of o the o(TermC.parse thy))"boundVariable b";
9.46 + val (dsc,id) = ((Model_Pattern.split_descriptor ctxt) o Thm.term_of o the o(TermC.parse thy))"boundVariable v_";
9.47 upd thy envv dsc (id, vl) i;
9.48 val it = (2,[(Free ("v_", "RealDef.real"),[Free ("b", "RealDef.real")])])
9.49 : int * (term * term list) list*)