1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Mon Apr 06 11:44:36 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Wed Apr 08 12:32:51 2020 +0200
     1.3 @@ -77,9 +77,9 @@
     1.4    | Check_elementwise of Rule.cterm'
     1.5    | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
     1.6  
     1.7 -  | Derive of Rule_Set.rls'
     1.8 -  | Detail_Set of Rule_Set.rls'
     1.9 -  | Detail_Set_Inst of Selem.subs * Rule_Set.rls'
    1.10 +  | Derive of Rule_Set.identifier
    1.11 +  | Detail_Set of Rule_Set.identifier
    1.12 +  | Detail_Set_Inst of Selem.subs * Rule_Set.identifier
    1.13    | End_Detail
    1.14  
    1.15    | Empty_Tac
    1.16 @@ -93,8 +93,8 @@
    1.17  
    1.18    | Rewrite of Celem.thm''
    1.19    | Rewrite_Inst of Selem.subs * Celem.thm''
    1.20 -  | Rewrite_Set of Rule_Set.rls'
    1.21 -  | Rewrite_Set_Inst of Selem.subs * Rule_Set.rls'
    1.22 +  | Rewrite_Set of Rule_Set.identifier
    1.23 +  | Rewrite_Set_Inst of Selem.subs * Rule_Set.identifier
    1.24  
    1.25    | Specify_Method of Celem.metID
    1.26    | Specify_Problem of Celem.pblID
    1.27 @@ -111,7 +111,7 @@
    1.28    val eq_tac : input * input -> bool
    1.29    val is_rewtac : input -> bool
    1.30    val is_rewset : input -> bool
    1.31 -  val rls_of : input -> Rule_Set.rls'
    1.32 +  val rls_of : input -> Rule_Set.identifier
    1.33    val rule2tac : theory -> (term * term) list ->  Rule.rule -> input
    1.34    val input_from_T : T -> input
    1.35    val result : T -> term
    1.36 @@ -165,9 +165,9 @@
    1.37    | Check_elementwise of Rule.cterm'
    1.38    | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
    1.39  
    1.40 -  | Derive of Rule_Set.rls'                 (* WN0509 drop *)
    1.41 -  | Detail_Set of Rule_Set.rls'             (* WN0509 drop *)
    1.42 -  | Detail_Set_Inst of Selem.subs * Rule_Set.rls' (* WN0509 drop *)
    1.43 +  | Derive of Rule_Set.identifier                 (* WN0509 drop *)
    1.44 +  | Detail_Set of Rule_Set.identifier             (* WN0509 drop *)
    1.45 +  | Detail_Set_Inst of Selem.subs * Rule_Set.identifier (* WN0509 drop *)
    1.46    | End_Detail                     (* WN0509 drop *)
    1.47  
    1.48    | Empty_Tac
    1.49 @@ -185,8 +185,8 @@
    1.50       and thm is created from ThmID by assoc_thm'' when entering isabisac *)
    1.51    | Rewrite of Celem.thm''
    1.52    | Rewrite_Inst of Selem.subs * Celem.thm''
    1.53 -  | Rewrite_Set of Rule_Set.rls'
    1.54 -  | Rewrite_Set_Inst of Selem.subs * Rule_Set.rls'
    1.55 +  | Rewrite_Set of Rule_Set.identifier
    1.56 +  | Rewrite_Set_Inst of Selem.subs * Rule_Set.identifier
    1.57  
    1.58    | Specify_Method of Celem.metID
    1.59    | Specify_Problem of Celem.pblID