1.1 --- a/src/Tools/isac/BaseDefinitions/contextC.sml	Wed Jan 11 11:38:01 2023 +0100
     1.2 +++ b/src/Tools/isac/BaseDefinitions/contextC.sml	Wed Jan 25 15:52:33 2023 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4    val isac_ctxt : 'a -> Proof.context
     1.5    val declare_constraints: term -> Proof.context -> Proof.context
     1.6    val add_constraints: term list -> Proof.context -> Proof.context
     1.7 +  val build_while_parsing: Formalise.model -> theory -> term list * Proof.context
     1.8    val initialise : Proof.context -> term list -> Proof.context
     1.9    val initialise' : theory -> TermC.as_string list -> Proof.context
    1.10    val get_assumptions : Proof.context -> term list
    1.11 @@ -37,7 +38,20 @@
    1.12  fun add_constraints ts ctxt =
    1.13    fold Variable.declare_constraints (TermC.vars' ts) ctxt
    1.14  
    1.15 +fun build_while_parsing_ [] (ts, ctxt) = (ts, ctxt)
    1.16 +  | build_while_parsing_ (str :: strs) (ts, ctxt) = 
    1.17 +    let
    1.18 +      val t as (_ $ tm) = Syntax.read_term ctxt str
    1.19 +        handle ERROR msg => raise ERROR ("ContextC.build_while_parsing " ^ quote str ^ " " ^ msg)
    1.20 +      val vars = TermC.vars tm
    1.21 +      val ctxt' = add_constraints vars ctxt
    1.22 +    in build_while_parsing_ strs (ts @ [t], ctxt') end
    1.23 +(* shouldn't that be done by fold ?
    1.24 +   fn: string * Proof.context -> term list * Proof.context -> term list * Proof.context *)
    1.25 +fun build_while_parsing strs thy = build_while_parsing_ strs ([], Proof_Context.init_global thy)
    1.26 +
    1.27  (* in Subproblem take respective actual arguments from program *)
    1.28 +(* FIXME: should be replaced by build_while_parsing *)
    1.29  fun initialise ctxt ts =
    1.30    let
    1.31      val frees = TermC.vars' ts