1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Sat May 02 10:57:04 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Sat May 02 11:36:13 2020 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4    | Add_Relation' of TermC.as_string * Model.itm list
     1.5    | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
     1.6  (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
     1.7 -(*RM*)| Init_Proof' of TermC.as_string list * Spec.T
     1.8    | Model_Problem' of Problem.id * Model.itm list * Model.itm list
     1.9    | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
    1.10    | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
    1.11 @@ -50,7 +49,6 @@
    1.12    | Add_Relation of TermC.as_string
    1.13    | Apply_Method of Method.id
    1.14    | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
    1.15 -  | Init_Proof of TermC.as_string list * Spec.T
    1.16    | Model_Problem
    1.17    | Refine_Problem of Problem.id
    1.18    | Refine_Tacitly of Problem.id
    1.19 @@ -118,7 +116,6 @@
    1.20      Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
    1.21    | Apply_Method of Method.id
    1.22    | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
    1.23 -  | Init_Proof of TermC.as_string list * Spec.T
    1.24    | Model_Problem
    1.25    | Refine_Problem of Problem.id
    1.26    | Refine_Tacitly of Problem.id
    1.27 @@ -148,9 +145,7 @@
    1.28    | End_Proof';
    1.29  
    1.30  fun input_to_string ma = case ma of
    1.31 -    Init_Proof (ppc, spec)  => 
    1.32 -      "Init_Proof "^(pair2str (strs2str ppc, Spec.to_string spec))
    1.33 -  | Model_Problem           => "Model_Problem "
    1.34 +    Model_Problem           => "Model_Problem "
    1.35    | Refine_Tacitly pblID    => "Refine_Tacitly " ^ strs2str pblID 
    1.36    | Refine_Problem pblID    => "Refine_Problem " ^ strs2str pblID 
    1.37    | Add_Given cterm'        => "Add_Given " ^ cterm'
    1.38 @@ -320,7 +315,6 @@
    1.39        Istate_Def.T *   (* for starting the Program                           *)
    1.40        Proof.context    (* for starting the Program                           *)
    1.41  (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
    1.42 -(*RM*)| Init_Proof' of TermC.as_string list * Spec.T
    1.43    | Model_Problem' of  (* first step in specify-phase                        *)
    1.44        Problem.id *     (* id in the Know_Store                               *)
    1.45        Model.itm list * (* the model for the Problem                          *)
    1.46 @@ -376,8 +370,7 @@
    1.47    | End_Proof''
    1.48  
    1.49  fun string_of ma = case ma of
    1.50 -    Init_Proof' (ppc, spec)  => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.to_string spec)
    1.51 -  | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
    1.52 +    Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
    1.53    | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
    1.54      strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
    1.55    | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
    1.56 @@ -472,8 +465,7 @@
    1.57  
    1.58  fun insert_assumptions tac ctxt  = ContextC.insert_assumptions (creates_assms tac) ctxt
    1.59  
    1.60 -fun for_specify (Init_Proof _) = true
    1.61 -  | for_specify Model_Problem  = true
    1.62 +fun for_specify Model_Problem  = true
    1.63    | for_specify (Refine_Tacitly _) = true
    1.64    | for_specify (Refine_Problem _) = true
    1.65    | for_specify (Add_Given _) = true
    1.66 @@ -486,8 +478,7 @@
    1.67    | for_specify (Specify_Problem _) = true
    1.68    | for_specify (Specify_Method _) = true
    1.69    | for_specify _ = false
    1.70 -fun for_specify' (Init_Proof' _) = true
    1.71 -  | for_specify' (Model_Problem' _) = true
    1.72 +fun for_specify' (Model_Problem' _) = true
    1.73    | for_specify' (Refine_Tacitly' _) = true
    1.74    | for_specify' (Refine_Problem' _) = true
    1.75    | for_specify' (Add_Given' _) = true