1.1 --- a/src/Tools/isac/Interpret/mstools.sml	Wed Sep 18 09:54:53 2013 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mstools.sml	Thu Sep 19 11:13:39 2013 +0200
     1.3 @@ -153,9 +153,7 @@
     1.4      val vts_in : itm list -> int list
     1.5     (* val w_itms2str_ : Proof.context -> itm list -> unit *)
     1.6      val get_assumptions : Proof.context -> term list
     1.7 -    val get_environments : Proof.context -> (term * term) list
     1.8      val insert_assumptions : term list -> Proof.context -> Proof.context
     1.9 -    val insert_environments : (term * term) list -> Proof.context -> Proof.context
    1.10      val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context
    1.11      val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context
    1.12   
    1.13 @@ -971,32 +969,11 @@
    1.14        val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
    1.15      in fold Variable.declare_constraints ts ctxt end;
    1.16  
    1.17 -datatype Isac_Ctxt =
    1.18 -    Env of term * term (*WN1105 unused*)
    1.19 -  | Asm of term;
    1.20 -
    1.21 -structure ContextData = Proof_Data
    1.22 -  (type T = Isac_Ctxt list
    1.23 +structure Context_Data = Proof_Data
    1.24 +  (type T = term list
    1.25     fun init _ = []);
    1.26 -
    1.27 -local
    1.28 -  fun unpack_asms (Asm t::ts) = t::(unpack_asms ts)
    1.29 -    | unpack_asms (Env _::ts) = unpack_asms ts
    1.30 -    | unpack_asms [] = [];
    1.31 -  fun unpack_envs (Env t::ts) = t::(unpack_envs ts)
    1.32 -    | unpack_envs (Asm _::ts) = unpack_envs ts
    1.33 -    | unpack_envs [] = [];
    1.34 -in
    1.35 -  fun get_assumptions ctxt = ContextData.get ctxt |> unpack_asms;
    1.36 -  fun get_environments ctxt = ContextData.get ctxt |> unpack_envs;
    1.37 -end
    1.38 -
    1.39 -local
    1.40 -  fun insert_ctxt data = ContextData.map (fn xs => distinct (data@xs));
    1.41 -in
    1.42 -  fun insert_assumptions asms = map (fn t => Asm t) asms |> insert_ctxt;
    1.43 -  fun insert_environments envs = map (fn t => Env t) envs |> insert_ctxt;
    1.44 -end
    1.45 +fun get_assumptions ctxt = Context_Data.get ctxt
    1.46 +fun insert_assumptions asms = Context_Data.map (fn xs => distinct (asms @ xs))
    1.47  
    1.48  (* transfer assumptions from one to another ctxt.
    1.49     does NOT respect scope: in a calculation identifiers are unique.

     2.1 --- a/test/Tools/isac/Interpret/mstools.sml	Wed Sep 18 09:54:53 2013 +0200
     2.2 +++ b/test/Tools/isac/Interpret/mstools.sml	Thu Sep 19 11:13:39 2013 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  "--------------------------------------------------------";
     2.5  "----------- fun declare_constraints' -------------------";
     2.6  "----------- fun declare_constraints --------------------";
     2.7 -"----------- fun get_assumptions, fun get_environments --";
     2.8 +"----------- fun get_assumptions, fun insert_assumptions-";
     2.9  "----------- fun transfer_asms_from_to ------------------";
    2.10  "----------- fun from_subpbl_to_caller ------------------";
    2.11  "----------- all ctxt changes in minimsubpbl x+1=2 ------";
    2.12 @@ -60,22 +60,14 @@
    2.13    if (t' |> type_of) = TFree ("'a", ["Num.numeral"]) then ()
    2.14    else error "Variable.declare_constraints did not recognize numeral";
    2.15  
    2.16 -"----------- fun get_assumptions, fun get_environments --";
    2.17 -"----------- fun get_assumptions, fun get_environments --";
    2.18 -"----------- fun get_assumptions, fun get_environments --";
    2.19 -val ctxt = insert_assumptions
    2.20 -      [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;
    2.21 -val ctxt = insert_assumptions
    2.22 -      [@{term "x * v"}, @{term "2 * u"}] ctxt;
    2.23 +"----------- fun get_assumptions, fun insert_assumptions-";
    2.24 +"----------- fun get_assumptions, fun insert_assumptions-";
    2.25 +"----------- fun get_assumptions, fun insert_assumptions-";
    2.26 +val ctxt = insert_assumptions [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;
    2.27 +val ctxt = insert_assumptions [@{term "x * v"}, @{term "2 * u"}] ctxt;
    2.28  val asms = get_assumptions ctxt;
    2.29 -if asms = [@{term "x * v"}, @{term "2 * u"}] then ()
    2.30 -else error "mstools.sml insert_/get_assumptions changed 1.";
    2.31 -
    2.32 -val ctxt = insert_environments
    2.33 -      [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] ctxt;
    2.34 -val envs = get_environments ctxt;
    2.35 -if envs = [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] then ()
    2.36 -else error "mstools.sml insert_/get_environments changed 2.";
    2.37 +if asms = [@{term "x * v"}, @{term "2 * u"}]
    2.38 +then () else error "mstools.sml insert_/get_assumptions changed 1.";
    2.39  
    2.40  "----------- fun transfer_asms_from_to ------------------";
    2.41  "----------- fun transfer_asms_from_to ------------------";