1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Fri Apr 10 15:02:50 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Fri Apr 10 16:16:09 2020 +0200
     1.3 @@ -77,9 +77,9 @@
     1.4    | Check_elementwise of TermC.as_string
     1.5    | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
     1.6  
     1.7 -  | Derive of Rule_Set.identifier
     1.8 -  | Detail_Set of Rule_Set.identifier
     1.9 -  | Detail_Set_Inst of Selem.subs * Rule_Set.identifier
    1.10 +  | Derive of Rule_Set.id
    1.11 +  | Detail_Set of Rule_Set.id
    1.12 +  | Detail_Set_Inst of Selem.subs * Rule_Set.id
    1.13    | End_Detail
    1.14  
    1.15    | Empty_Tac
    1.16 @@ -93,8 +93,8 @@
    1.17  
    1.18    | Rewrite of ThmC_Def.thm''
    1.19    | Rewrite_Inst of Selem.subs * ThmC_Def.thm''
    1.20 -  | Rewrite_Set of Rule_Set.identifier
    1.21 -  | Rewrite_Set_Inst of Selem.subs * Rule_Set.identifier
    1.22 +  | Rewrite_Set of Rule_Set.id
    1.23 +  | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
    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.identifier
    1.32 +  val rls_of : input -> Rule_Set.id
    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 TermC.as_string
    1.38    | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
    1.39  
    1.40 -  | Derive of Rule_Set.identifier                 (* WN0509 drop *)
    1.41 -  | Detail_Set of Rule_Set.identifier             (* WN0509 drop *)
    1.42 -  | Detail_Set_Inst of Selem.subs * Rule_Set.identifier (* WN0509 drop *)
    1.43 +  | Derive of Rule_Set.id                 (* WN0509 drop *)
    1.44 +  | Detail_Set of Rule_Set.id             (* WN0509 drop *)
    1.45 +  | Detail_Set_Inst of Selem.subs * Rule_Set.id (* 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 ThmC_Def.thm''
    1.52    | Rewrite_Inst of Selem.subs * ThmC_Def.thm''
    1.53 -  | Rewrite_Set of Rule_Set.identifier
    1.54 -  | Rewrite_Set_Inst of Selem.subs * Rule_Set.identifier
    1.55 +  | Rewrite_Set of Rule_Set.id
    1.56 +  | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
    1.57  
    1.58    | Specify_Method of Celem.metID
    1.59    | Specify_Problem of Celem.pblID
    1.60 @@ -315,11 +315,11 @@
    1.61    | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
    1.62    | rule2tac _ subst (Rule.Thm thm'') = 
    1.63      Rewrite_Inst (Selem.subst2subs subst, thm'')
    1.64 -  | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.rls2str rls)
    1.65 +  | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls)
    1.66    | rule2tac _ subst (Rule.Rls_ rls) = 
    1.67 -    Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.rls2str rls))
    1.68 +    Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.id rls))
    1.69    | rule2tac _ _ rule = 
    1.70 -    error ("rule2tac: called with \"" ^ Rule.rule2str rule ^ "\"");
    1.71 +    error ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\"");
    1.72  
    1.73  (* tactics for for internal use, compare "input" for user at the front-end.
    1.74    tac_ contains results from check in 'fun applicable_in'.
    1.75 @@ -437,12 +437,12 @@
    1.76    | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
    1.77    | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
    1.78    | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
    1.79 -    "," ^ Rule_Set.rls2str rls' ^ "," ^ UnparseC.term2str f ^ ",(" ^ UnparseC.term2str f' ^ "," ^ UnparseC.terms2str asm ^ "))"
    1.80 +    "," ^ Rule_Set.id rls' ^ "," ^ UnparseC.term2str f ^ ",(" ^ UnparseC.term2str f' ^ "," ^ UnparseC.terms2str asm ^ "))"
    1.81    | End_Detail' _ => "End_Detail' xxx"
    1.82    | Detail_Set' _ => "Detail_Set' xxx"
    1.83    | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
    1.84  
    1.85 -  | Derive' rls => "Derive' " ^ Rule_Set.rls2str rls
    1.86 +  | Derive' rls => "Derive' " ^ Rule_Set.id rls
    1.87    | Calculate'  _ => "Calculate' "
    1.88    | Substitute' _ => "Substitute' "(*^(subs2str subs)*)    
    1.89  
    1.90 @@ -468,13 +468,13 @@
    1.91    | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
    1.92    | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Selem.subst2subs sub, thm)
    1.93  
    1.94 -  | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.rls2str rls)
    1.95 -  | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.rls2str rls)
    1.96 +  | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id rls)
    1.97 +  | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.id rls)
    1.98  
    1.99    | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) = 
   1.100 -    Rewrite_Set_Inst (Selem.subst2subs sub, Rule_Set.rls2str rls)
   1.101 +    Rewrite_Set_Inst (Selem.subst2subs sub, Rule_Set.id rls)
   1.102    | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) = 
   1.103 -    Detail_Set_Inst (Selem.subst2subs sub, Rule_Set.rls2str rls)
   1.104 +    Detail_Set_Inst (Selem.subst2subs sub, Rule_Set.id rls)
   1.105  
   1.106    | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
   1.107    | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred