1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Nov 25 12:44:43 2020 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Nov 25 16:10:24 2020 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4    val is_closed: theory -> bool
     1.5  end;
     1.6  
     1.7 -structure SPARK_VCs: SPARK_VCS =
     1.8 +structure SPARK_VCs(** ): SPARK_VCS( **) =
     1.9  struct
    1.10  
    1.11  open Fdl_Parser;

     2.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Wed Nov 25 12:44:43 2020 +0100
     2.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Wed Nov 25 16:10:24 2020 +0100
     2.3 @@ -1009,8 +1009,10 @@
     2.4          ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))] => xxx
     2.5        | _ => error "magic failed: handling file exp_Statics_Biegel_Timischl_7-70.str failed"
     2.6    (*\----- keep running from spark_open \<open>greatest_common_divisor/g_c_d\<close> -----/*)
     2.7 -    val (hdl, (dI, pI, mI), pors, pctxt) = Step_Specify.initialisePIDE formalise
     2.8 -      (* ^^^ for CAS_Cmd only,    ^^^^^ do NOT use: UPDATE thy's context with O_Model.values*)
     2.9 +    val (hdl, (dI, pI, mI), pors, frees, _) = Step_Specify.initialisePIDE formalise
    2.10 +      (* ^^^ for CAS_Cmd only     ^^^^^ from ContextC.initialise'*)
    2.11 +
    2.12 +
    2.13      val prfx' =
    2.14        if opt_prfx = "" then
    2.15          space_implode "__" (Long_Name.explode (Long_Name.qualifier ident))

     3.1 --- a/src/Tools/isac/Specify/step-specify.sml	Wed Nov 25 12:44:43 2020 +0100
     3.2 +++ b/src/Tools/isac/Specify/step-specify.sml	Wed Nov 25 16:10:24 2020 +0100
     3.3 @@ -9,7 +9,7 @@
     3.4    val by_tactic_input: Tactic.input -> Calc.T -> string * Calc.state_post
     3.5    val by_tactic: Tactic.T -> Calc.T -> string * Calc.state_post
     3.6  
     3.7 -  val initialisePIDE: Formalise.T -> term * References.T * O_Model.T * Proof.context
     3.8 +  val initialisePIDE: Formalise.T -> term * References.T * O_Model.T * term list * Proof.context
     3.9    val nxt_specify_init_calc: Formalise.T -> Calc.T * State_Steps.T
    3.10  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    3.11    (*NONE*)
    3.12 @@ -220,24 +220,26 @@
    3.13  	      if mI = ["no_met"] 
    3.14  	      then 
    3.15            let 
    3.16 -            val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy;
    3.17 -            val pctxt = ContextC.initialise' thy fmz;
    3.18 +            val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy; (*..TermC.parseNEW'*)
    3.19 +            val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)
    3.20  		        val pI' = Refine.refine_ori' pors pI;
    3.21  		      in (pI', (pors (*refinement over models with diff.precond only*), pctxt),
    3.22  		        (hd o #met o Problem.from_store) pI')
    3.23  		      end
    3.24  	      else
    3.25  	        let
    3.26 -	          val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy;
    3.27 -            val pctxt = ContextC.initialise' thy fmz;
    3.28 +	          val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy; (*..TermC.parseNEW'*)
    3.29 +            val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)
    3.30  	        in (pI, (pors, pctxt), mI) end;
    3.31  	    val {cas, ppc, thy = thy', ...} = Problem.from_store pI (*take dI from _refined_ pbl*)
    3.32  	    val dI = Context.theory_name (ThyC.sub_common (thy, thy'))
    3.33  	    val hdl = case cas of
    3.34  		    NONE => Auto_Prog.pblterm dI pI
    3.35  		  | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
    3.36 +		  val frees = map (TermC.parseNEW' (Proof_Context.init_global thy)) fmz |> TermC.vars'
    3.37 +		                       (*^^^^^^^^^                                   DUPLICATE ermC.parseNEW'*)
    3.38      in
    3.39 -      (hdl, (dI, pI, mI), pors, pctxt)
    3.40 +      (hdl, (dI, pI, mI), pors, frees, pctxt)
    3.41      end;
    3.42  (*  nxt_specify_init_calc \<rightarrow> initialise *)
    3.43  fun nxt_specify_init_calc ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)
    3.44 @@ -273,7 +275,7 @@
    3.45  	      in ((pt, ([], Pbl)), []) end
    3.46    | nxt_specify_init_calc (fmz, (dI, pI, mI)) = 
    3.47      let            (* both ^^^  ^^^^^^^^^^^^  are either empty or complete *)
    3.48 -	    val (hdl, (dI, pI, mI), pors, pctxt) = initialisePIDE (fmz, (dI, pI, mI))
    3.49 +	    val (hdl, (dI, pI, mI), pors, _, pctxt) = initialisePIDE (fmz, (dI, pI, mI))
    3.50        val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)
    3.51          (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl, pctxt)
    3.52      in