1.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml	Mon Jul 19 15:34:54 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml	Mon Jul 19 17:29:35 2021 +0200
     1.3 @@ -257,9 +257,9 @@
     1.4  if UnparseC.term t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then ()
     1.5  else error "rule2stac_inst Thm.. changed";
     1.6  case t of
     1.7 -  (Const ("Tactical.Try", _) $
     1.8 -    (Const ("Tactical.Repeat", _) $
     1.9 -      (Const ("Prog_Tac.Rewrite_Inst", _) $
    1.10 +  (Const (\<^const_name>\<open>Try\<close>, _) $
    1.11 +    (Const (\<^const_name>\<open>Repeat\<close>, _) $
    1.12 +      (Const (\<^const_name>\<open>Rewrite_Inst\<close>, _) $
    1.13          (Const (\<^const_name>\<open>Cons\<close>, _) $
    1.14            (Const (\<^const_name>\<open>Pair\<close>, _) $
    1.15              bdv $
    1.16 @@ -277,12 +277,12 @@
    1.17  "-------- fun stacpbls, fun eval_leaf -----------------------------------";
    1.18  val {scr, ...} = MethodC.from_store ["Test", "sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
    1.19  case stacpbls sc of
    1.20 -  [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,
    1.21 -   Const ("Prog_Tac.Rewrite_Set", _) $ Test_simplify,
    1.22 -   Const ("Prog_Tac.Rewrite_Set", _) $ rearrange_assoc,
    1.23 -   Const ("Prog_Tac.Rewrite_Set", _) $ isolate_root,
    1.24 -   Const ("Prog_Tac.Rewrite_Set", _) $ norm_equation,
    1.25 -   Const ("Prog_Tac.Rewrite_Set_Inst", _) $
    1.26 +  [Const (\<^const_name>\<open>Rewrite\<close>, _) $ square_equation_left,
    1.27 +   Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ Test_simplify,
    1.28 +   Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ rearrange_assoc,
    1.29 +   Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ isolate_root,
    1.30 +   Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ norm_equation,
    1.31 +   Const (\<^const_name>\<open>Rewrite_Set_Inst\<close>, _) $
    1.32       (Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ bdv $ Free ("v_v", _)) $
    1.33         Const (\<^const_name>\<open>Nil\<close>, _)) $ isolate_bdv] => 
    1.34       if HOLogic.dest_string square_equation_left = "square_equation_left" andalso