1.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml	Fri May 07 13:23:24 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml	Fri May 07 18:12:51 2021 +0200
     1.3 @@ -154,26 +154,26 @@
     1.4  *** . Free (t_t, 'z)
     1.5  *** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
     1.6  *** . . Const (Program.Try, ('a => 'a) => 'a => 'a)
     1.7 -*** . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
     1.8 +*** . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
     1.9  *** . . . . Free (discard_minus, ID)
    1.10  *** . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
    1.11  *** . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
    1.12 -*** . . . . Const (Program.Rewrite'_Set, ID  => 'a => 'a)
    1.13 +*** . . . . Const (Program.Rewrite_Set, ID  => 'a => 'a)
    1.14  *** . . . . . Free (rat_mult_poly, ID)
    1.15  *** . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
    1.16  *** . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
    1.17 -*** . . . . . Const (Program.Rewrite'_Set, ID  => 'a => 'a)
    1.18 +*** . . . . . Const (Program.Rewrite_Set, ID  => 'a => 'a)
    1.19  *** . . . . . . Free (make_rat_poly_with_parentheses, ID)
    1.20  *** . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
    1.21  *** . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
    1.22 -*** . . . . . . Const (Program.Rewrite'_Set, ID  => 'a => 'a)
    1.23 +*** . . . . . . Const (Program.Rewrite_Set, ID  => 'a => 'a)
    1.24  *** . . . . . . . Free (cancel_p_rls, ID)
    1.25  *** . . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
    1.26  *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
    1.27 -*** . . . . . . . Const (Program.Rewrite'_Set, ID  => 'a => 'a)
    1.28 +*** . . . . . . . Const (Program.Rewrite_Set, ID  => 'a => 'a)
    1.29  *** . . . . . . . . Free (norm_Rational_rls, ID)
    1.30  *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
    1.31 -*** . . . . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
    1.32 +*** . . . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
    1.33  *** . . . . . . . . Free (discard_parentheses1, ID)
    1.34  *** . . Const (empty, 'a)
    1.35  ***)
    1.36 @@ -259,7 +259,7 @@
    1.37  case t of
    1.38    (Const ("Tactical.Try", _) $
    1.39      (Const ("Tactical.Repeat", _) $
    1.40 -      (Const ("Prog_Tac.Rewrite'_Inst", _) $
    1.41 +      (Const ("Prog_Tac.Rewrite_Inst", _) $
    1.42          (Const ("List.list.Cons", _) $
    1.43            (Const ("Product_Type.Pair", _) $
    1.44              bdv $
    1.45 @@ -278,11 +278,11 @@
    1.46  val {scr, ...} = MethodC.from_store ["Test", "sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
    1.47  case stacpbls sc of
    1.48    [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,
    1.49 -   Const ("Prog_Tac.Rewrite'_Set", _) $ Test_simplify,
    1.50 -   Const ("Prog_Tac.Rewrite'_Set", _) $ rearrange_assoc,
    1.51 -   Const ("Prog_Tac.Rewrite'_Set", _) $ isolate_root,
    1.52 -   Const ("Prog_Tac.Rewrite'_Set", _) $ norm_equation,
    1.53 -   Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $
    1.54 +   Const ("Prog_Tac.Rewrite_Set", _) $ Test_simplify,
    1.55 +   Const ("Prog_Tac.Rewrite_Set", _) $ rearrange_assoc,
    1.56 +   Const ("Prog_Tac.Rewrite_Set", _) $ isolate_root,
    1.57 +   Const ("Prog_Tac.Rewrite_Set", _) $ norm_equation,
    1.58 +   Const ("Prog_Tac.Rewrite_Set_Inst", _) $
    1.59       (Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ bdv $ Free ("v_v", _)) $
    1.60         Const ("List.list.Nil", _)) $ isolate_bdv] => 
    1.61       if HOLogic.dest_string square_equation_left = "square_equation_left" andalso